coe_eq_zero_iff — Mathlib

English

For any χ in weights, the linear functional χ represented by χ on L is zero if and only if χ is the zero weight.

Русский

Для любого χ из весов линейный функционал, задаваемый χ на L, равен нулю тогда и только тогда, когда χ — нулевой вес.

LaTeX

$$$(χ : L \to R) = 0 \;\iff\; χ.IsZero$$$

Lean4

@[simp]
theorem coe_eq_zero_iff (χ : Weight R L M) : (χ : L → R) = 0 ↔ χ.IsZero :=
  Iff.rfl

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