Theorem StructureGroupoid.LocalInvariantProp.congr_set_fun

Modification history

2026-06-11 13:02
Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
feat: drop `HasGroupoid` assumption in several `LiftPropAt` lemmas (#40475)
Added StructureGroupoid.LocalInvariantProp.congr_set_funView on Github →