Commit 2021-02-02 11:46 75a7ce9f

View on Github →

refactor(*): rename subtype_congr to subtype_equiv (#6004) This definition is closely related to perm.subtype_perm, so renaming will bring them closer in use. Also releavnt is #5875 which defines a separate perm.subtype_congr.

Estimated changes

Modified src/category_theory/adjunction/lifting.lean

Modified src/category_theory/monad/monadicity.lean

Modified src/data/equiv/basic.lean

deleted def equiv.subtype_congr

deleted theorem equiv.subtype_congr_apply

deleted def equiv.subtype_congr_prop

deleted def equiv.subtype_congr_right

deleted theorem equiv.subtype_congr_symm_apply

added def equiv.subtype_equiv

added theorem equiv.subtype_equiv_apply

added def equiv.subtype_equiv_prop

added def equiv.subtype_equiv_right

added theorem equiv.subtype_equiv_symm_apply

Modified src/data/fintype/card.lean

Modified src/field_theory/finite/polynomial.lean

Modified src/ring_theory/polynomial/symmetric.lean