Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-28 04:53 7b253dd5

View on Github →

feat(group_theory/subgroup): lemmas for normal subgroups of subgroups (#7271)

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem monoid_hom.comap_bot

modified theorem monoid_hom.range_restrict_ker

added theorem subgroup.coe_subgroup_of

modified theorem subgroup.comap_injective

modified theorem subgroup.comap_map_eq

modified theorem subgroup.comap_map_eq_self

modified theorem subgroup.comap_map_eq_self_of_injective

added theorem subgroup.comap_sup_comap_le

added theorem subgroup.comap_sup_eq

added theorem subgroup.inf_mul_assoc

added theorem subgroup.inf_subgroup_of_inf_normal_of_left

added theorem subgroup.inf_subgroup_of_inf_normal_of_right

modified theorem subgroup.ker_le_comap

modified theorem subgroup.le_comap_map

modified theorem subgroup.map_comap_eq

modified theorem subgroup.map_comap_eq_self

modified theorem subgroup.map_comap_eq_self_of_surjective

modified theorem subgroup.map_comap_le

modified theorem subgroup.map_eq_comap_of_inverse

added theorem subgroup.map_inf_eq

added theorem subgroup.map_inf_le

modified theorem subgroup.map_injective

added theorem subgroup.map_injective_of_ker_le

modified theorem subgroup.map_le_range

added theorem subgroup.mem_subgroup_of

added theorem subgroup.mul_inf_assoc

added theorem subgroup.normal_subgroup_of_iff

added theorem subgroup.subgroup_normal.mem_comm

added def subgroup.subgroup_of

added theorem subgroup.subgroup_of_map_subtype

added theorem subgroup.subgroup_of_sup

added theorem subgroup.supr_comap_le