Commit 2022-12-11 13:46 4f4e7fa6

View on Github →

feat(group_theory/perm/basic): subtype_perm is a monoid hom (#17816) A few more subtype_perm lemmas. Clean up the subtype_perm section. Rename equiv.perm.default_perm to equiv.perm.default_eq.

Estimated changes

Modified src/group_theory/perm/basic.lean

added theorem equiv.perm.default_eq

deleted theorem equiv.perm.default_perm

added theorem equiv.perm.inv_subtype_perm

modified theorem equiv.perm.mem_iff_of_subtype_apply_mem

modified def equiv.perm.of_subtype

modified theorem equiv.perm.of_subtype_apply_coe

modified theorem equiv.perm.of_subtype_apply_of_mem

modified theorem equiv.perm.of_subtype_apply_of_not_mem

modified theorem equiv.perm.of_subtype_subtype_perm

modified theorem equiv.perm.subtype_equiv_subtype_perm_apply_of_mem

modified theorem equiv.perm.subtype_equiv_subtype_perm_apply_of_not_mem

modified def equiv.perm.subtype_perm

modified theorem equiv.perm.subtype_perm_apply

added theorem equiv.perm.subtype_perm_inv

added theorem equiv.perm.subtype_perm_mul

modified theorem equiv.perm.subtype_perm_of_subtype

modified theorem equiv.perm.subtype_perm_one

added theorem equiv.perm.subtype_perm_pow

added theorem equiv.perm.subtype_perm_zpow

Modified src/group_theory/perm/cycle/basic.lean

Modified src/group_theory/perm/sign.lean