Commit 2025-04-17 08:00 d4fc0372

View on Github →

chore: deprecate the file AnalyticManifold (#20979) It's now superseded by the generic IsManifold.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Deprecated/AnalyticManifold.lean

added def analyticGroupoid

added theorem analyticGroupoid_prod

added def analyticPregroupoid

added theorem mem_analyticGroupoid

added theorem mem_analyticGroupoid_of_boundaryless

added theorem ofSet_mem_analyticGroupoid

added theorem symm_trans_mem_analyticGroupoid

Modified Mathlib/Geometry/Manifold/AnalyticManifold.lean

deleted def analyticGroupoid

deleted theorem analyticGroupoid_prod

deleted def analyticPregroupoid

deleted theorem mem_analyticGroupoid

deleted theorem mem_analyticGroupoid_of_boundaryless

deleted theorem ofSet_mem_analyticGroupoid

deleted theorem symm_trans_mem_analyticGroupoid