Commit 2022-09-30 08:02 d610cec7

View on Github →

feat(group_theory/quotient_group): simp lemmas for quotient_group.map (#16703) Little lemmas that I needed to work with the class group of a ring of integers.

Estimated changes

Modified src/group_theory/quotient_group.lean

added theorem quotient_group.map_comp_map

added theorem quotient_group.map_id

added theorem quotient_group.map_id_apply

added theorem quotient_group.map_map

Modified src/group_theory/subgroup/basic.lean

added theorem subgroup.comap_id