instFree

Mathlib.Algebra.QuadraticAlgebra

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

English

The quadratic algebra is a free R-module with a basis given by basis a b.

Русский

Квадратичная алгебра является свободным модулем над R с базисом basis a b.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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