mathlib3

91ca9270 - feat(geometry/manifold/local_invariant_properties): local structomorphism is `local_invariant_prop` (#3434)

feat(geometry/manifold/local_invariant_properties): local structomorphism is `local_invariant_prop` (#3434) For a groupoid `G`, define the property of being a local structomorphism; prove that if `G` is closed under restriction then this property satisfies `local_invariant_prop` (i.e., is local and `G`-invariant).