Commit 2021-10-26 17:54 3aa57492

View on Github →

feat(group_theory/subgroup/basic): Define characteristic subgroups (#9921) This PR defines characteristic subgroups and builds the basic API. Getting @[to_additive] to work correctly was a bit tricky, so I mostly just copied the setup for subgroup.normal.

Estimated changes

Modified src/data/equiv/mul_add_aut.lean

modified theorem add_aut.conj_apply

Modified src/group_theory/nilpotent.lean

Modified src/group_theory/solvable.lean

Modified src/group_theory/subgroup/basic.lean

added structure add_subgroup.characteristic

added structure subgroup.characteristic

added theorem subgroup.characteristic_iff_comap_eq

added theorem subgroup.characteristic_iff_comap_le

added theorem subgroup.characteristic_iff_le_comap

added theorem subgroup.characteristic_iff_le_map

added theorem subgroup.characteristic_iff_map_eq

added theorem subgroup.characteristic_iff_map_le