IsZero — Mathlib

English

IsZero is the proposition that a weight χ satisfies χ = 0 as a function L → R; equivalently χ is the zero weight.

Русский

IsZero — это утверждение, что вес χ равен нулю как функция L → R; то есть χ — нулевой вес.

LaTeX

$$IsZero(χ) := (χ : L → R) = 0$$

Lean4

/-- The proposition that a weight of a Lie module is zero.

We make this definition because we cannot define a `Zero (Weight R L M)` instance since the weight
space of the zero function can be trivial. -/
def IsZero (χ : Weight R L M) :=
  (χ : L → R) = 0

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