Commit 2023-06-25 10:23 99b23050

View on Github →

feat: port Geometry.Manifold.Algebra.Structures (#5453)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

Modified Mathlib/Geometry/Manifold/Algebra/Monoid.lean

modified theorem L_mul

modified theorem R_mul

Created Mathlib/Geometry/Manifold/Algebra/Structures.lean

added theorem topologicalSemiring_of_smooth

Modified Mathlib/Geometry/Manifold/ContMDiffMap.lean