Commit 2024-06-14 08:06 449179b4

View on Github →

refactor: move analyticGroupoid to a new file AnalyticManifold.lean (#13785) It used to be in SmoothManifoldWithCorners.lean, but this makes no sense as nothing downstream of that file uses analyticGroupoid. In #10853, I will rewrite the definition of analyticGroupoid and define AnalyticManifold on top of it.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/AnalyticManifold.lean

added def analyticGroupoid

added theorem mem_analyticGroupoid_of_boundaryless

added theorem ofSet_mem_analyticGroupoid

added theorem symm_trans_mem_analyticGroupoid

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

deleted def analyticGroupoid

deleted theorem mem_analyticGroupoid_of_boundaryless

deleted theorem ofSet_mem_analyticGroupoid

deleted theorem symm_trans_mem_analyticGroupoid