Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-07 05:56 91824e58

View on Github →

feat(group_theory/subgroup): Normal Core (#8940) Defines normal core, and proves lemmas analogous to those for normal closure.

Estimated changes

Modified src/group_theory/group_action/basic.lean

added theorem subgroup.normal_core_eq_ker

Modified src/group_theory/subgroup.lean

added def subgroup.normal_core

added theorem subgroup.normal_core_eq_self

added theorem subgroup.normal_core_eq_supr

added theorem subgroup.normal_core_idempotent

added theorem subgroup.normal_core_le

added theorem subgroup.normal_core_mono

added theorem subgroup.normal_le_normal_core