wInner_cWeight_eq_one_iff_eq — Mathlib

English

If the Boole inner product equals 1, then ψ1 = ψ2; i.e., equality of characters is detected by the inner product.

Русский

Если внутреннее произведение равно 1, то ψ1 = ψ2; тождество чар определяется этим внутренним произведением.

LaTeX

$$$⟪ψ_1, ψ_2⟫_{R}^{\\text{cWeight}} = 1 \\Rightarrow ψ_1 = ψ_2.$$$

Lean4

theorem wInner_cWeight_eq_one_iff_eq [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = 1 ↔ ψ₁ = ψ₂ := by
  rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_left_iff]

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