Elementwise centrality of the Frattini layer

Section7FrattiniCentral proves the subgroup statement ⁅K, Φ(K)⁆ = ⊥. The tower packets need the elementwise field r * k = k * r for r ∈ Φ(K) and k ∈ K. This file is the direct bridge.

theorem Q2Presentation.Induction.kernelFrattini_central_in_K {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (r : p.fst.Y) : r ∈ kernelFrattini K → ∀ k ∈ K.Ksub, r * k = k * r

Elementwise form of kernel_commutator_frattini_eq_bot: the literal Frattini layer Φ(K) centralizes the minimal kernel K.