zero_apply — Mathlib

English

The weight corresponding to zero is the zero function when the weight space is nontrivial: the weight χ=0 gives a function χ(x) = 0 for all x.

Русский

Вес, соответствующий нулю, является нулевой функцией, если весовое пространство ненулево: χ(x) = 0 для всех x.

LaTeX

$$$((0:\\mathrm{Weight}\\;R\\;L\\;M) : L \\to R) = 0$$$

Lean4

theorem zero_apply [Nontrivial (genWeightSpace M (0 : L → R))] (x) : (0 : Weight R L M) x = 0 :=
  rfl

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