Commit 2021-09-15 18:42 2b589cad

View on Github →

feat(group_theory/subgroup): Generalize comap_sup_eq (#9212) The lemma comap_sup_eq can be generalized from assuming function.surjective f to assuming ≤ f.range.

Estimated changes

Modified src/group_theory/subgroup.lean

modified theorem subgroup.comap_sup_eq

added theorem subgroup.comap_sup_eq_of_le_range

added theorem subgroup.sup_subgroup_of_eq