zero_notMem_range_root

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

theorem zero_notMem_range_root [NeZero (2 : R)] : 0 ∉ range P.root := by
  simpa only [mem_range, not_exists] using fun i ↦ P.ne_zero i

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

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

Разделы

Аффилиация

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