nontrivial

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

If there exists a nonzero root, then the module M is nontrivial (not the zero module).

Русский

Если существует ненулевой корень, то модуль M ненулевой (не нулевой модуль).

LaTeX

$$$ M \neq \{0\} $$$

Lean4

protected theorem nontrivial [Nonempty ι] [NeZero (2 : R)] : Nontrivial M :=
  by
  obtain ⟨i, hi⟩ := P.exists_ne_zero
  exact ⟨P.root i, 0, hi⟩

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

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

Разделы

Аффилиация

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