Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-05 05:31 81618883

View on Github →

feat(group_theory/subgroup): define normal bundled subgroups (#2947) Most proofs are adapted from deprecated/subgroup.

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem add_subgroup.sub_mem

added theorem monoid_hom.normal_ker

deleted theorem monoid_hom.rang_top_of_surjective

added theorem monoid_hom.range_top_of_surjective

added theorem subgroup.bot_normal

added def subgroup.center

added theorem subgroup.center_normal

modified theorem subgroup.coe_inv

added theorem subgroup.coe_mk

added theorem subgroup.le_normalizer

added theorem subgroup.le_normalizer_of_normal

added theorem subgroup.mem_center_iff

added theorem subgroup.mem_normalizer_iff

added theorem subgroup.mul_mem_cancel_left

added theorem subgroup.mul_mem_cancel_right

added theorem subgroup.normal.conj_mem

added theorem subgroup.normal.mem_comm

added theorem subgroup.normal.mem_comm_iff

added theorem subgroup.normal_in_normalizer

added theorem subgroup.normal_of_comm

added def subgroup.normalizer