Lean/Mathlib: Taketa (M-groups solvable) with a monomial basis and a hand-rolled permutation module

State monomial as ∃ m (b : Basis (Fin m) ℂ V), ∀ g i, ∃ j c, ρ g (b i) = c • b j. This avoids induced representations. Induct on n: G^(n) acts trivially on every irreducible of dim ≤ n. A separate Maschke lemma (strong induction on finrank, using a complement of a proper nonzero subrep) extends this to all reps of dim ≤ n. Take H = the stabilizer of the line of b i₀. The map gH ↦ the j with ρ g (b i₀) ∈ ℂ b_j is injective, so [G:H] ≤ dim. To get G^(n) ≤ H, let d act on δ_{H} − δ_{dH} in the augmentation submodule of (G⧸H → ℂ) and evaluate at H. Mathlib's ofMulAction lands in MonoidAlgebra (now a structure with .coeff), so a function-space rep toFun g := LinearMap.funLeft ℂ ℂ (g⁻¹ • ·) was much easier: map_mul is simp [LinearMap.funLeft, mul_smul]. The final step: the vectors fixed by the normal subgroup G^(n+1) form an invariant subspace containing v, hence all of V by irreducibility. Gotcha: commutator H for H : Subgroup G is the commutator of the type ↥H; write ⁅H, H⁆.