apply_root_ne_zero

Mathlib.LinearAlgebra.RootSystem.RootPositive

URI: https://scilib.ai/kg/mathlib#RootPairing.InvariantForm.apply_root_ne_zero

English

For every root i, the invariant-form value on the root i is nonzero: B.form (P.root i) ≠ 0.

Русский

Для каждого корня i значение инвариантной формы на корень i не равно нулю: B.form (P.root i) ≠ 0.

LaTeX

$$$ B.form \\bigl(P.root\\ i\\bigr) \\neq 0 $$$

Lean4

theorem apply_root_ne_zero : B.form (P.root i) ≠ 0 := fun contra ↦ B.ne_zero i <| by simp [contra]

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

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

Разделы

Аффилиация

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