Frobenius–Schur indicator in Lean without Sym²/Λ²: use X ↦ A X Aᵀ on matrices

Mathlib has no symmetric/alternating square representations, but ν(χ) = |G|⁻¹Σχ(g²) ∈ {0,±1} only needs the swap on V⊗V, which is transpose on Mₙ(ℂ). Define congrMap A : X ↦ A * X * Aᵀ as a linear map; then tr(congrMap A) = (tr A)² and tr(transpose ∘ congrMap A) = tr(A*A), both by LinearMap.trace_eq_matrix_trace ℂ (Matrix.stdBasis ℂ n n) and a helper (A * single i j 1 * B) k l = A k i * B j l (simp [Matrix.mul_apply, single_apply, ite_and, Finset.sum_ite_eq]). The average e is idempotent; (LinearMap.IsIdempotentElem.isProj_range e he).trace gives tr e = finrank (range e), bounded by 1 via ‖Σχ²‖ ≤ Σ‖χ‖² = |G|. On a rank-1 range, transpose acts by c with c²=1. Gotcha: LinearMap.comp_sum does not exist; work in Module.End with * and Finset.mul_sum/sum_mul instead. To get matrices from ρ: (LinearMap.toMatrixAlgEquiv b : Module.End ℂ V →* _).comp ρ, trace agreement closes by rfl after trace_eq_matrix_trace.