coe_toLinear_ne_zero_iff

Mathlib.Algebra.Lie.Weights.Linear

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

English

A weight χ is nonzero iff its linear realization is nonzero.

Русский

Вес χ не нулевой тогда и только тогда, когда его линейная реализация не нулевая.

LaTeX

$$$χ \\neq 0 \\iff toLinear(χ) \\neq 0.$$$

Lean4

theorem coe_toLinear_ne_zero_iff : (χ : L →ₗ[R] R) ≠ 0 ↔ χ.IsNonZero := by simp

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

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

Разделы

Аффилиация

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