zero_notMem_range_coroot

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

0 does not lie in the image of the coroot map: 0 ∉ range P.coroot.

Русский

0 не лежит в образе карты коррота: 0 ∉ range P.coroot.

LaTeX

$$$ 0 \notin \operatorname{range}(P.coroot) $$$

Lean4

theorem zero_notMem_range_coroot [NeZero (2 : R)] : 0 ∉ range P.coroot :=
  P.flip.zero_notMem_range_root

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

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

Разделы

Аффилиация

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