Commit 2025-03-17 11:54 594019ab

View on Github →

refactor(Setoid/Basic): Use Relation.Map (#22981) This has the existential in a different order.

Estimated changes

Modified Mathlib/Data/Setoid/Basic.lean

modified def Setoid.mapOfSurjective

Modified Mathlib/GroupTheory/Congruence/Defs.lean

Modified Mathlib/Logic/Relation.lean

added theorem Relation.map_equivalence

added theorem Relation.map_mono

added theorem Relation.map_reflexive

added theorem Relation.map_transitive