instDirectSum

Mathlib.LinearAlgebra.DirectSum.Finite

URI: https://scilib.ai/kg/mathlib#Module.Finite.instDirectSum

English

If R ⊆ S is a quadratic extension, then finrank_R S = 2.

Русский

Если S является квадратичным расширениемR, то размерность S над R равна 2.

LaTeX

$$$\\operatorname{finrank} R S = 2$$$

Lean4

instance instDirectSum : Module.Finite R (⨁ i, M i) :=
  Module.Finite.instDFinsupp M

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

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

Разделы

Аффилиация

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