ne_zero'

Mathlib.LinearAlgebra.RootSystem.Defs

URI: https://scilib.ai/kg/mathlib#RootPairing.ne_zero'

English

For a fixed i, the coroot component in N is nonzero: (P.coroot i) ≠ 0.

Русский

Для фиксированного индекса i компонент_coroot в N не равен нулю: (P.coroot i) ≠ 0.

LaTeX

$$$ (P.coroot i : N) \neq 0 $$$

Lean4

theorem ne_zero' [NeZero (2 : R)] : (P.coroot i : N) ≠ 0 :=
  P.flip.ne_zero i

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

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

Разделы

Аффилиация

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