wInner_cWeight_self — Mathlib

English

If G is finite, the family of functions (ψ ↦ (ψ: G→R) as ψ runs AddChar G R) is linearly independent; hence the dimension of the span is card of AddChar.

Русский

Если G конечна, семейство функций ψ ↦ ψ является линейно независимым; размерности пространства порождаемого этим семейством не больше cardinalAddChar.

LaTeX

$$$\\text{LinearIndependent}_{\\mathbb{R}}(\\{\\psi \\mapsto (\\psi) : \\psi \\in \\operatorname{AddChar}(G,R)\\})$ при конечном G.$$

Lean4

theorem wInner_cWeight_self (ψ : AddChar G R) : ⟪(ψ : G → R), ψ⟫ₙ_[R] = 1 := by
  simp [wInner_cWeight_eq_expect, ψ.norm_apply, RCLike.mul_conj]

Похожие утверждения