theorem
Hex.PermGroup.Group.normalClosure_le_subgroup
{n : ℕ}
(G H : Group n)
(h : H.IsSubgroup G)
(N : Subgroup ↥(closure G.generators))
[N.Normal]
(hN : (closure H.generators).subgroupOf (closure G.generators) ≤ N)
:
The insertion trace lies in every mathematical normal subgroup containing the input, without requiring an executable presentation of that subgroup.
theorem
Hex.PermGroup.Group.normalClosure_spec
{n : ℕ}
(G H : Group n)
(h : H.IsSubgroup G)
:
(closure (G.normalClosure H h).generators).subgroupOf (closure G.generators) = Subgroup.normalClosure ↑((closure H.generators).subgroupOf (closure G.generators))
The computational normal closure is Mathlib's normal closure inside the ambient generated subgroup. All conjugation takes place in that group.
theorem
Hex.PermGroup.Group.core_spec
{n : ℕ}
(G H : Group n)
(h : H.IsSubgroup G)
:
(closure (G.core H h).generators).subgroupOf (closure G.generators) = ((closure H.generators).subgroupOf (closure G.generators)).normalCore
Complete intersection replay identifies the core with Mathlib's greatest normal subgroup contained in the input.