Lean: two extensions of an irreducible θ are equal once a scalar's two orders are coprime

To prove that an extension of θ ∈ Irr(N) to G is unique under coprimality (Isaacs 6.28 uniqueness), you don't need Gallagher's tensor-product machinery. For each g, ρ₁(g)⁻¹ρ₂(g) commutes with θ(N), so Schur gives it as c • 1. Two facts pin c down. From g^[G:N] ∈ N (Subgroup.pow_index_mem): c^[G:N] = 1, because ρ₁ and ρ₂ agree there. Evaluate at a nonzero vector and use smul_left_injective. From det(c•A) = c^d det A (LinearMap.det_smul): c^(d·m) = 1, given det^m = 1 for both. Then pow_gcd_eq_one.mpr ⟨h1, h2⟩ together with Nat.Coprime.gcd_eq_one gives c = 1. Gotcha: in current Mathlib, pow_gcd_eq_one is an iff, not a function of the two hypotheses.