Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 20:04 a80e5683

View on Github →

feat(logic/equiv/set): equivalences between all preimages gives an equivalence of domains (#13853)

Estimated changes

Modified src/data/fintype/card.lean

Modified src/group_theory/coset.lean

Modified src/group_theory/group_action/basic.lean

Modified src/group_theory/p_group.lean

Modified src/logic/equiv/basic.lean

added def equiv.of_fiber_equiv

added theorem equiv.of_fiber_equiv_map

added def equiv.sigma_fiber_equiv

deleted def equiv.sigma_preimage_equiv

added def equiv.sigma_subtype_fiber_equiv

added def equiv.sigma_subtype_fiber_equiv_subtype

deleted def equiv.sigma_subtype_preimage_equiv

deleted def equiv.sigma_subtype_preimage_equiv_subtype

Modified src/logic/equiv/set.lean

added def equiv.of_preimage_equiv

added theorem equiv.of_preimage_equiv_map

added def equiv.sigma_preimage_equiv

Modified src/logic/small.lean

Modified src/set_theory/cardinal/basic.lean