IsNonZero

Mathlib.Algebra.Lie.Weights.Basic

URI: https://scilib.ai/kg/mathlib#LieModule.Weight.IsNonZero

English

IsNonZero χ is defined as the negation of χ being zero: χ.IsNonZero ⇔ ¬ χ.IsZero.

Русский

IsNonZero χ определяется как отрицание χ.IsZero: χ.IsNonZero ⇔ ¬ χ.IsZero.

LaTeX

$$IsNonZero χ := ¬ IsZero χ$$

Lean4

/-- The proposition that a weight of a Lie module is non-zero. -/
abbrev IsNonZero (χ : Weight R L M) :=
  ¬IsZero (χ : Weight R L M)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru