Commit 2024-05-21 20:03 84acd2b4

View on Github →

feat(StructureGroupoid): one small lemma and some docstrings (#9827) I added an iff version of mem_of_eqOnSource. This is to mirror how lemmas like HasDerivAt.congr_of_eventuallyEq have an iff counterpart Filter.EventuallyEq.hasDerivAt_iff. I also wrote the docstrings for fields of StructureGroupoid.

<!-- The text above the `

Estimated changes

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

added theorem StructureGroupoid.mem_iff_of_eqOnSource

Modified scripts/nolints.json