eq — Mathlib · SciLib

English

If χ is a zero weight, then χ, regarded as a linear functional on L, is identically zero; that is, χ(l) = 0 for every l ∈ L.

Русский

Если χ — нулевой вес, то χ, рассматриваемый как линейный функционал на L, тождественно равен нулю; то есть χ(l) = 0 для всех l ∈ L.

LaTeX

$$$\text{If } χ.IsZero,\; (χ : L \to R) = 0$$$

Lean4

@[simp]
theorem eq {χ : Weight R L M} (hχ : χ.IsZero) : (χ : L → R) = 0 :=
  hχ

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