instFree

Mathlib.Algebra.SkewMonoidAlgebra.Basic

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

English

SkewMonoidAlgebra k G is a free k-module with basis given by basisSingleOne.

Русский

SkewMonoidAlgebra k G является свободным модулем над k с базисом basisSingleOne.

LaTeX

$$$ \text{Module.Free } k (SkewMonoidAlgebra k G) $$$

Lean4

instance [Semiring k] : Module.Free k (SkewMonoidAlgebra k G) :=
  Module.Free.of_basis basisSingleOne

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

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

Разделы

Аффилиация

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