Skip to content

Don't look up!#39597

Open
grunweg wants to merge 703 commits into
leanprover-community:masterfrom
grunweg:experiements-miretreat
Open

Don't look up!#39597
grunweg wants to merge 703 commits into
leanprover-community:masterfrom
grunweg:experiements-miretreat

Conversation

@grunweg

@grunweg grunweg commented May 19, 2026

Copy link
Copy Markdown
Contributor

Open in Gitpod

grunweg and others added 30 commits March 3, 2026 17:11
@grunweg
Torsion as a 2-tensor
43dd396
@hrmacbeth
start new approach to levi-civita
6082ae3
@hrmacbeth
addition theorem for tensor construction
00b1995
@hrmacbeth
finish proof of addition lemma
c7c2212
@grunweg
Progress towards LC being a connection
a84d21f
@hrmacbeth
construct difference of connections using tensoriality constructor
410bb87
@hrmacbeth
tensor apply lemmas
876ce4f
@hrmacbeth
hacky proofs
f195851
@hrmacbeth
make this the definition of levi-civita connection
12255d0
@hrmacbeth
bit of cleanup
bee9d66
@grunweg
Merge branch 'master' into hm-covder-bundled
224be51
@grunweg
First round of fixes
4dd83df
@grunweg
Further
6ac17e7
@grunweg
Further
5c96bb7
@hrmacbeth @grunweg
down to one sorry
83643af
@hrmacbeth @grunweg
last sorry in lc file
a19ae15
@hrmacbeth @grunweg
golf using linear_combination
b4d4d12
@hrmacbeth @grunweg
golf
51a8380
@grunweg
Fix the build of LeviCivita
f357252
@grunweg
Fix Lift
58e15e9
@PatrickMassot
Try to catch up
32a6e22
@grunweg
chore: split out Extend
20a011e
@grunweg
chore: move tensor definitions to tensoriality
5b94048
@grunweg
chore: move torsion lemmas using local frames to a separate file
feaaa2b 
They will be refactored later anyway.
@grunweg
chore: minimise imports in (Triv)Prelim
8a1fa83
@grunweg
chore: split material about Ehresmann connections part into a new file
d22f9af
@grunweg
chore: move material about trivial bundles to a separate file
3c5af5b
@grunweg
Fix and tweak imports more
1739941
@grunweg
chore: move mfderiv lemmas we need to a separate file
f6079a3
@hrmacbeth
reorganise variables in tensoriality file
ebd0377
hrmacbeth and others added 25 commits May 16, 2026 04:27
@hrmacbeth
adjust curvature file to general bundle
2536088
@hrmacbeth
fix
134699a
@grunweg
wip: add mvfderinvWithin with (d)elaborators and corresponding lemmas
fc679b6
@grunweg
feat: mfderivWithin_{add,neg,sub}
6662a03
@grunweg
Finish proving corresponding mvfderivWithin lemmas
34ae1ad
@grunweg
chore: name the right lemma to set up fun_prop; comment this
4db8033
@grunweg
Fix one variable warning
cc51360
@grunweg
Merge branch 'master' into hm-covder-bundled
e53d7d0
@PatrickMassot
More ∇ notation
f909a6c 
I’m really not sure we want this. I only push this discussion
@PatrickMassot
Random cleanups and move around
dfecc14
@PatrickMassot
Remove one layer of auxiliary definition
3bc62f4
@grunweg
Merge branch 'master' into hm-covder-bundled
3e5070b
@grunweg
Fixup, mfderivWithin_neg should have f implicit
f638335
@grunweg
Merge branch 'master' into hm-covder-bundled
f005ace
@grunweg
Remove to_fun workaround
11ce3ce
@grunweg
Merge branch 'master' into hm-covder-bundled
317a86a
@grunweg
Remove more to_fun workaround
f5bbf82
@grunweg
RFC: use notation d% and d[ for mvfderiv(Within)
5dec592 
It's getting really clean now... is the notation clear enough?
@hrmacbeth
sharpen typeclasses
3dace16
@hrmacbeth
allow for variant regularity in extensionality lemmas
be8d17d
@hrmacbeth
look at curvature file
6e48700
@grunweg
chore: sync with in-flight changes in leanprover-community#39513
5295127
@grunweg
chore: make fromTangentSpace lemmas private
1e1dc7b 
- we can also make mfderiv_smul private
- as a matter of fact, half our smul lemmas are now superfluous, given that
  we can hide behind the mvfderiv abstraction! \o/

- also use mvfderiv instead of open-coding it in CovariantDerivative/Trivial
@grunweg
chore(Curvature): fix two warnings; use T% more
e4d16b8
@grunweg
experiment: playing with notation for mvfderiv and better hovers
0190b25
@github-actions github-actions Bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-differential-geometry Manifolds etc labels May 19, 2026
@github-actions

github-actions Bot commented May 19, 2026 •
edited
Loading

Copy link
Copy Markdown

🚨 PR Title Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

error: the PR title does not contain a colon
Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

  • feat (feature)
  • fix (bug fix)
  • doc (documentation)
  • style (formatting, missing semicolons, ...)
  • refactor
  • test (when adding missing tests)
  • chore (maintain)
  • perf (performance improvement, optimization, ...)
  • ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

  • Data/Nat/Basic
  • Algebra/Group/Defs
  • Topology/Constructions

<subject> has the following constraints:

  • do not capitalize the first letter
  • no dot(.) at the end
  • use imperative, present tense: "change" not "changed" nor "changes"

@grunweg grunweg added the WIP Work in progress label May 19, 2026
@grunweg grunweg changed the title Experiements miretreat Don't look up! May 19, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-differential-geometry Manifolds etc WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@grunweg @hrmacbeth @PatrickMassot