toRootSystem

Mathlib.LinearAlgebra.RootSystem.Irreducible

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

Lean4

/-- A nonempty irreducible root pairing is a root system. -/
def toRootSystem [Nonempty ι] [NeZero (2 : R)] [P.IsIrreducible] : RootSystem ι R M N :=
  { toRootPairing := P
    span_root_eq_top :=
      IsIrreducible.eq_top_of_invtSubmodule_reflection (P.rootSpan R) P.rootSpan_mem_invtSubmodule_reflection
        (P.rootSpan_ne_bot R)
    span_coroot_eq_top :=
      IsIrreducible.eq_top_of_invtSubmodule_coreflection (P.corootSpan R) P.corootSpan_mem_invtSubmodule_coreflection
        (P.corootSpan_ne_bot R) }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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