instFinite

Mathlib.Algebra.QuadraticAlgebra

URI: https://scilib.ai/kg/mathlib#QuadraticAlgebra.instFinite

English

The QuadraticAlgebra R a b is a finite R-module with a basis indexed by Fin 2.

Русский

Квадратичная алгебра по отношению к R является конечным модулем над R, имеющим базис, индексируемый Fin 2.

LaTeX

$$$Module.Finite R (QuadraticAlgebra R a b)$$$

Lean4

instance : Module.Finite R (QuadraticAlgebra R a b) :=
  .of_basis (basis a b)

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

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

Разделы

Аффилиация

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