Commit 2022-11-18 00:38 92ded3bc

View on Github →

feat: port logic.equiv.defs (#550) mathlib3 sha: 7951ed37deb3b2923a6f47d9bdcb4d69a8703550 Waiting on the release of nightly-2022-11-17.

Estimated changes

deleted theorem Equiv.apply_symm_apply
deleted theorem Equiv.coe_fn_mk
deleted theorem Equiv.inv_fun_as_coe
deleted def Equiv.perm
deleted def Equiv.refl
deleted theorem Equiv.self_comp_symm
deleted def Equiv.symm
deleted theorem Equiv.symm_apply_apply
deleted theorem Equiv.symm_comp_self
deleted def Equiv.trans
deleted structure Equiv
added theorem Equiv.Perm.ext
added theorem Equiv.Perm.ext_iff
added def Equiv.Perm
added theorem Equiv.apply_eq_iff_eq
added theorem Equiv.apply_symm_apply
added theorem Equiv.arrowCongr'_refl
added theorem Equiv.arrowCongr'_symm
added def Equiv.arrowCongr
added theorem Equiv.arrowCongr_comp
added theorem Equiv.arrowCongr_refl
added theorem Equiv.arrowCongr_symm
added theorem Equiv.arrowCongr_trans
added theorem Equiv.bijective_comp
added theorem Equiv.cast_apply
added theorem Equiv.cast_eq_iff_heq
added theorem Equiv.cast_refl
added theorem Equiv.cast_symm
added theorem Equiv.cast_trans
added theorem Equiv.coe_fn_injective
added theorem Equiv.coe_fn_symm_mk
added theorem Equiv.coe_refl
added theorem Equiv.coe_trans
added theorem Equiv.comp_bijective
added theorem Equiv.comp_injective
added theorem Equiv.comp_surjective
added theorem Equiv.comp_symm_eq
added def Equiv.conj
added theorem Equiv.conj_comp
added theorem Equiv.conj_refl
added theorem Equiv.conj_symm
added theorem Equiv.conj_trans
added theorem Equiv.eq_comp_symm
added theorem Equiv.eq_symm_apply
added theorem Equiv.eq_symm_comp
added def Equiv.equivCongr
added theorem Equiv.equivCongr_refl
added theorem Equiv.equivCongr_symm
added theorem Equiv.equivCongr_trans
added def Equiv.equivEmpty
added def Equiv.equivPUnit
added theorem Equiv.ext
added theorem Equiv.ext_iff
added def Equiv.funUnique
added theorem Equiv.injective_comp
added theorem Equiv.inv_fun_as_coe
added theorem Equiv.nonempty_congr
added def Equiv.ofIff
added def Equiv.permCongr
added theorem Equiv.permCongr_apply
added theorem Equiv.permCongr_def
added theorem Equiv.permCongr_refl
added theorem Equiv.permCongr_symm
added theorem Equiv.permCongr_trans
added theorem Equiv.refl_apply
added theorem Equiv.refl_symm
added theorem Equiv.refl_trans
added theorem Equiv.self_comp_symm
added theorem Equiv.self_trans_symm
added def Equiv.sigmaAssoc
added def Equiv.sigmaCongr
added theorem Equiv.surjective_comp
added theorem Equiv.symm_apply_apply
added theorem Equiv.symm_apply_eq
added theorem Equiv.symm_comp_eq
added theorem Equiv.symm_comp_self
added theorem Equiv.symm_symm
added theorem Equiv.symm_symm_apply
added theorem Equiv.symm_trans_apply
added theorem Equiv.symm_trans_self
added theorem Equiv.trans_apply
added theorem Equiv.trans_assoc
added theorem Equiv.trans_refl
added structure Equiv
added theorem Quot.congr_mk
added theorem Quotient.congr_mk
modified def uniqueProp