Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-10 00:06 f1df14c2

View on Github →

feat(group_theory/subgroup): normal_closure and gpowers (#2959) Transfer some more proofs from deprecated/subgroup

Estimated changes

deleted def group.conjugates
deleted theorem group.mem_conjugates_self
deleted theorem injective_mul
added theorem add_subgroup.coe_gsmul
added theorem add_subgroup.coe_smul
added structure add_subgroup.normal
added def group.conjugates
modified theorem monoid_hom.normal_ker
modified def monoid_hom.range
modified theorem subgroup.bot_normal
added theorem subgroup.coe_gpow
modified theorem subgroup.coe_inv
modified theorem subgroup.coe_mk
modified theorem subgroup.coe_mul
modified theorem subgroup.coe_one
added theorem subgroup.coe_pow
added def subgroup.gpowers
added theorem subgroup.mem_gpowers
added theorem subgroup.normal.comap
deleted theorem subgroup.normal.conj_mem
added structure subgroup.normal
added theorem subgroup.normal_comap
added def subgroup.of_div