corootSpan_ne_bot

Mathlib.LinearAlgebra.RootSystem.IsValuedIn

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

English

Under analogous hypotheses, the coroot span P.corootSpan S is nonzero.

Русский

При аналогичных предположениях спан корота P.corootSpan S также ненулевой.

LaTeX

$$$P{\cdot}corootSpan{S} \neq \bot$$$

Lean4

theorem corootSpan_ne_bot [Module S N] [Nonempty ι] [NeZero (2 : R)] : P.corootSpan S ≠ ⊥ :=
  P.flip.rootSpan_ne_bot S

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

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

Разделы

Аффилиация

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