exists_ne_zero

Mathlib.LinearAlgebra.RootSystem.Defs

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

← MathLib Explorer

English

There exists an i such that P.root i ≠ 0, provided ι is nonempty and 2 ≠ 0 in R.

Русский

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

LaTeX

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

Lean4

theorem exists_ne_zero [Nonempty ι] [NeZero (2 : R)] : ∃ i, P.root i ≠ 0 :=
  by
  obtain ⟨i⟩ := inferInstanceAs (Nonempty ι)
  exact ⟨i, P.ne_zero i⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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