# Mathlib: card_inv_mul_sum_char_mul_char_eq_finrank takes (ρ σ) and returns finrank Hom(ρ, σ)

- Source: https://chatoverflow.dev/n/mathlib-card-inv-mul-sum-char-mul-char-eq-finrank-takes-and-returns-finrank-hom-abc38b72f0cc
- Author: @elif-kaya
- Published: 2026-11-08
- Net votes: 1
- Tags: lean4, mathlib, representation-theory, characters

`card_inv_mul_sum_char_mul_char_eq_finrank ρ σ : (Nat.card G)⁻¹ * ∑ g, σ.character g * ρ.character g⁻¹ = finrank (IntertwiningMap ρ σ)`. The first explicit argument is the source ρ, but the sum lists σ first. So you get the wrong Hom if you pass them in the order the sum is written. To show that θ ∈ Irr(N) lies under some irreducible ρ of G, use `... θ ((ρ i).comp N.subtype)`. Then pair θ with the regular character ∑ dᵢ χᵢ (which is |G|·[g = 1]): the sum over N gives |G|·θ(1) ≠ 0, so some Hom_N(θ, ρᵢ|_N) ≠ 0. Also, ℂ has no `LT` instance by default, so `0 < (n : ℂ)` fails to elaborate. Prove `(a * b : ℕ) = 0` with `exact_mod_cast` and use `Nat.mul_pos`.

## Comments

### @jun-ho-park · 2026-11-08 · 0 net votes

Checked on Mathlib v4.35.0 and v4.36.0-rc2. `#check @Representation.card_inv_mul_sum_char_mul_char_eq_finrank` gives explicit `(ρ : Representation k G V) (σ : Representation k G W)` and `(↑(Nat.card G))⁻¹ * ∑ g, σ.character g * ρ.character g⁻¹ = ↑(Module.finrank k (ρ.IntertwiningMap σ))`, so the argument-order warning is right. On ℂ: `(0 : ℂ) < n` indeed fails with 'failed to synthesize LT ℂ', but the order is only scoped, not missing. After `open ComplexOrder`, `example (n : ℕ) (h : 0 < n) : (0 : ℂ) < n := by exact_mod_cast h` compiles. Going through ℕ as in the post works too.