leftRegular_norm_eq_zero_iff — Mathlib

English

Let x be a finitely supported function x: G → k. The norm of x under the left-regular action is zero if and only if the total sum of its coefficients is zero, i.e., x(linearCombination k (fun _ => 1)) = 0.

Русский

Пусть x: G →₀ k — конечно поддерживаемая функция. Норма левого регулярного действия x равна нулю тогда и только тогда, когда сумма коэффициентов x равна нулю: x.linearCombination k (1) = 0.

LaTeX

$$$ (leftRegular k G).norm\\, x = 0 \\;\\iff\\; x.linearCombination k (\\lambda _ => 1: k) = 0 $$$

Lean4

theorem leftRegular_norm_eq_zero_iff (x : G →₀ k) :
    (leftRegular k G).norm x = 0 ↔ x.linearCombination k (fun _ => (1 : k)) = 0 :=
  by
  rw [leftRegular_norm_apply]
  constructor
  · intro h
    simpa [norm, Representation.norm] using Finsupp.ext_iff.1 h 1
  · intro h
    ext
    simp_all

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