Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: port Geometry.Manifold.ContMdiffMfderiv #5496

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat: port Geometry.Manifold.ContMdiffMfderiv #5496

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
16e46e1
feat: port Geometry.Manifold.ContMdiffMfderiv
urkud Jul 5, 2023
c5508dd
Initial file copy from mathport
urkud Jul 5, 2023
4132285
automated fixes
urkud Jul 5, 2023
5a8f2a4
Rename file
urkud Jun 26, 2023
37f2c8a
A section was moved to `MFDeriv`, first fixes
urkud Jun 26, 2023
d5a7a74
Snapshot
urkud Jun 27, 2023
566e393
Small fixes
urkud Jul 5, 2023
8104942
Trailing whitespace
urkud Jul 5, 2023
7c92de9
Cherry-pick some fixes
urkud Jul 5, 2023
703af66
Fix compile
urkud Jul 12, 2023
441ebfb
auto: naming
urkud Jul 12, 2023
947452e
Fix style linter
urkud Jul 12, 2023
a1623ca
Update Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
urkud Jul 13, 2023
5d64a04
Update Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
urkud Jul 13, 2023
6126811
Apply suggestions from code review
urkud Jul 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1891,6 +1891,7 @@ import Mathlib.Geometry.Manifold.ChartedSpace
import Mathlib.Geometry.Manifold.Complex
import Mathlib.Geometry.Manifold.ConformalGroupoid
import Mathlib.Geometry.Manifold.ContMDiff
import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
import Mathlib.Geometry.Manifold.ContMDiffMap
import Mathlib.Geometry.Manifold.DerivationBundle
import Mathlib.Geometry.Manifold.Diffeomorph
Expand Down
Loading
Loading