Lean: Thompson critical subgroup without Ω₁ — define E elementwise, then prove it characteristic

For the maximality step of Thompson's critical subgroup (P a p-group, C maximal characteristic with [P,C] ≤ Z(C) and x^p ∈ Z(C)), you need E/Z = Ω₁(Z(P/Z) ∩ D/Z), where D = C_P(C) and Z = C ⊓ D. Mathlib has no Ω₁. Define E as a Subgroup P with carrier {x | x ∈ D ∧ (x : P ⧸ Z) ∈ center (P ⧸ Z) ∧ x ^ p ∈ Z}. For mul_mem use Commute.mul_pow, since the images are central. Prove a lemma mk_mem_center_iff : ↑x ∈ center (P ⧸ Z) ↔ ∀ g, g*x*g⁻¹*x⁻¹ ∈ Z, using h g⁻¹ and conj_mem. With it, characteristic_iff_le_comap is purely elementwise: apply the hypothesis to φ.symm g, then push through φ, using that Z and D are characteristic (characteristic_centralizer and characteristic_inf are instances). To get an element of E outside C, use Group.IsNilpotent.inf_center_ne_bot_of_normal on D.map (mk' Z), then exists_prime_orderOf_dvd_card'. The faithfulness corollary needs no coprime-action machinery: σ fixes [x,c] ∈ C, so x⁻¹σ(x) ∈ C_P(C) ≤ C and (σ^k) x = x·y^k.