Commit 2021-04-06 18:32 5f0dbf65

View on Github →

feat(algebra/group/conj): is_conj for monoids, is_conj.setoid, and conj_classes (#6896) Refactors is_conj to work in a monoid Defines is_conj.setoid and its quotient type, conj_classes

Estimated changes

Modified docs/undergrad.yaml

Modified src/algebra/char_p/invertible.lean

added theorem not_ring_char_dvd_of_invertible

deleted theorem ring_char_not_dvd_of_invertible

Modified src/algebra/group/conj.lean

added def conj_classes.carrier

added theorem conj_classes.carrier_eq_preimage_mk

added theorem conj_classes.exists_rep

added theorem conj_classes.forall_is_conj

added def conj_classes.map

added theorem conj_classes.mem_carrier_iff_mk_eq

added theorem conj_classes.mem_carrier_mk

added theorem conj_classes.mk_bijective

added theorem conj_classes.mk_eq_mk_iff_is_conj

added def conj_classes.mk_equiv

added theorem conj_classes.mk_injective

added theorem conj_classes.mk_surjective

added theorem conj_classes.one_eq_mk_one

added theorem conj_classes.quot_mk_eq_mk

added theorem conj_classes.quotient_mk_eq_mk

added def conj_classes

added def conjugates_of

added theorem is_conj.conjugates_of_eq

modified def is_conj

added theorem is_conj_iff'

added theorem is_conj_iff

added theorem is_conj_iff_conjugates_of_eq

modified theorem is_conj_iff_eq

added theorem mem_conjugates_of_self

Modified src/algebra/group/semiconj.lean

added theorem semiconj_by_iff_eq

Modified src/deprecated/subgroup.lean

added theorem group.conjugates_of_subset

deleted theorem group.conjugates_subset

Modified src/group_theory/perm/sign.lean

Modified src/group_theory/solvable.lean

Modified src/group_theory/subgroup.lean

deleted def group.conjugates

modified def group.conjugates_of_set

deleted theorem group.mem_conjugates_self

Modified src/representation_theory/maschke.lean