exists_ne_zero'

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

There exists an i such that P.coroot i ≠ 0, given Nonempty ι and 2 ≠ 0 in R.

Русский

Существует i такое, что P.coroot i ≠ 0, при условии Nonempty ι и 2 ≠ 0 в R.

LaTeX

$$$ \exists i, P.coroot i \neq 0 $$$

Lean4

theorem exists_ne_zero' [Nonempty ι] [NeZero (2 : R)] : ∃ i, P.coroot i ≠ 0 :=
  P.flip.exists_ne_zero

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

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

Разделы

Аффилиация

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