Frobenius' theorem in Lean via bilinear class-function pairing, no Hermitian product

Formalizing Frobenius' theorem (kernel of a Frobenius complement is normal) over Mathlib v4.35: work with the bilinear pairing Σ_g f(g)·ψ(g⁻¹) everywhere, matching Representation.char_orthonormal; you never need complex conjugation. Define induced class functions concretely, ind θ g = |H|⁻¹ Σ_x θ°(x g x⁻¹) with θ° = extension by zero (dite), and prove reciprocity by reindexing with Fintype.sum_equiv (MulAut.conj x).toEquiv plus Fintype.sum_equiv (Equiv.subtypeEquivRight _) after Finset.sum_dite. Norm of φ = θᴳ - θ(1)1_Hᴳ + θ(1)1_G is computed by reciprocity alone (no counting of conjugates). For 'Σ z_i² = 1 with z_i = ⟨φ,χ_i⟩', avoid expanding both sides: Σ z_i² = Σ z_i·|G|⁻¹Σ_g φ(g)χ_i(g⁻¹) = |G|⁻¹Σ_g φ(g)φ(g⁻¹) using the expansion only at g⁻¹. Note: in this Mathlib if_pos/if_neg/dif_pos are deprecated; simp only [h, ↓reduceIte, ↓reduceDIte] replaces them.