Lean: building a representation of G from θ on N and an operator A (cyclic G/N) without subtype pain

Task: extend a G-invariant irreducible θ : Representation ℂ N W to G when G/N is cyclic (Isaacs 11.22). Define θ̂(x) = A^k * θ(g^{-k} x).

What made it work: 1. Extend θ by zero to all of G: extEnd θ u := if h : u ∈ N then θ ⟨u, h⟩ else 0 (open scoped Classical). Then every identity is an equation of G-elements under extEnd, which group and congr 2 handle. Prove extEnd_mul (for hu, hv ∈ N) and extEnd_one once. 2. Pick m := Nat.find (∃ m, 0 < m ∧ g^m ∈ N); orderOf g works as a witness. Let kf x := Nat.find (∃ k < m, (g^k)⁻¹ * x ∈ N). The key lemma is that ANY j with (g^j)⁻¹ x ∈ N computes the same value: hF : F x = A^j * extEnd θ ((g^j)⁻¹ * x). Prove it by writing j = kf x + m*(j/m), using A^(m q) = extEnd θ (g^(m q)) (induction on q) and extEnd_mul. Once hF holds, map_one, map_mul (take j = a + b) and the restriction to N (take j = 0) are a few lines each. 3. For uniqueness of k < m use wlog h : j₁ ≤ j₂ generalizing j₁ j₂ with H, then g^(j₂-j₁) = (g^j₁)⁻¹x((g^j₂)⁻¹x)⁻¹ ∈ N and minimality of m. 4. Schur scalar without the algebraMap API: finrank_eq_one_iff_of_nonzero' (IntertwiningMap.id θ) hid applied to finrank_intertwiningMap_self gives c with c • id = C. For the m-th root use IsAlgClosed.exists_pow_nat_eq. 5. IsCyclic (T ⧸ N.subgroupOf T) from IsCyclic (G ⧸ N): isCyclic_of_injective (QuotientGroup.map _ _ T.subtype (fun n hn ↦ hn)) hinj. In the injectivity proof, rw [QuotientGroup.map_mk] failed (the term was not type-correct at implicit transparency). change ((a : G) : G ⧸ N) = ((b : G) : G ⧸ N) at hab followed by QuotientGroup.eq worked. 6. IsMulCommutative from IsCyclic: take a generator, write a = g^i and b = g^j via Subgroup.mem_zpowers_iff, then (Commute.zpow_zpow_self g i j).eq.