Lean: inertia group of θ ∈ Irr(K) in a Frobenius group is K, via Brauer's permutation lemma

Goal: for G = K ⋊ H Frobenius and 1 ≠ θ ∈ Irr(K), show θ^G is irreducible. In Lean the shortest route was to show the inertia group is K and then apply a Clifford correspondence or Mackey criterion lemma. The inertia group was defined as {x | ∀ n, θ.character (MulAut.conjNormal x n) = θ.character n}.

Step 1 (pure group theory): g ∉ K fixes no nontrivial K-class. From IsConj k (MulAut.conjNormal g k), isConj_iff gives c : K with c k c⁻¹ = g k g⁻¹. To move this to G, apply congrArg Subtype.val, then MulAut.conjNormal_apply, then simpa. y := g⁻¹ c ∉ K commutes with k. Unfolding the kernel definition {g | ∀ x, x g x⁻¹ ∈ H → g = 1} with not_forall gives x with x y x⁻¹ ∈ H \ 1, and that element commutes with x k x⁻¹ ∈ K. Step 2: Brauer's permutation lemma (number of fixed irreducible characters = number of fixed classes) gives exactly one fixed character. Show the fixed-class filter is {ConjClasses.mk 1}: use ConjClasses.mk_surjective for one direction, and ConjClasses.mk_eq_mk_iff_isConj with isConj_one_left for the other. Then Finset.card_eq_one gives {a}. The trivial-character index i0 and the index j of θ both lie in that singleton, so j = i0.

Gotchas: - To find the trivial rep in a character table you need IsIrreducible (trivial ℂ L ℂ). Build e : Subrepresentation (trivial ℂ L ℂ) ≃o Submodule ℂ ℂ (toFun S := S.toSubmodule, invFun p := ⟨p, fun _ _ hv ↦ by simpa using hv⟩, map_rel_iff' := Iff.rfl). Use e.isSimpleOrder, not e.symm.isSimpleOrder: OrderIso.isSimpleOrder transfers from the codomain to the domain. - Table lemmas quantified over W : Type pin universes, so state θ on W : Type.