Commit 2022-12-22 03:31 afe35920

View on Github →

feat: port algebra.group.conj (#1158) Port of algebra.group.conj Based on 0743cc5d9d86bcd1bba10f480e948a257d65056f

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Group/Conj.lean

added def ConjClasses.carrier

added theorem ConjClasses.carrier_eq_preimage_mk

added theorem ConjClasses.exists_rep

added theorem ConjClasses.forall_isConj

added def ConjClasses.map

added theorem ConjClasses.map_surjective

added theorem ConjClasses.mem_carrier_iff_mk_eq

added theorem ConjClasses.mem_carrier_mk

added def ConjClasses.mkEquiv

added theorem ConjClasses.mk_bijective

added theorem ConjClasses.mk_eq_mk_iff_isConj

added theorem ConjClasses.mk_injective

added theorem ConjClasses.mk_surjective

added theorem ConjClasses.one_eq_mk_one

added theorem ConjClasses.quot_mk_eq_mk

added theorem ConjClasses.quotient_mk_eq_mk

added def ConjClasses

added theorem IsConj.conjugatesOf_eq

added theorem IsConj.refl

added theorem IsConj.symm

added theorem IsConj.trans

added def IsConj

added theorem conj_injective

added theorem conj_inv

added theorem conj_mul

added theorem conj_pow

added theorem conj_zpow

added def conjugatesOf

added theorem isConj_comm

added theorem isConj_iff

added theorem isConj_iff_conjugatesOf_eq

added theorem isConj_iff_eq

added theorem isConj_iff₀

added theorem isConj_one_left

added theorem isConj_one_right

added theorem mem_conjugatesOf_self