nontrivial'

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

If there exists a nonzero coroot, then the module N is nontrivial.

Русский

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

LaTeX

$$$ N \neq \{0\} $$$

Lean4

protected theorem nontrivial' [Nonempty ι] [NeZero (2 : R)] : Nontrivial N :=
  P.flip.nontrivial

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

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

Разделы

Аффилиация

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