instFree

Mathlib.LinearAlgebra.Finsupp.VectorSpace

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

English

The AddMonoidAlgebra S ι is free over R with the finsupp-based freeness construction.

Русский

Модуль AddMonoidAlgebra S ι свободен над R; он свободен с базисом, полученным через конструкцию из Finsupp.

LaTeX

$$$\\text{Module.Free } R (\\mathrm{AddMonoidAlgebra}\\ S ι)$$$

Lean4

instance : Module.Free R S[ι] :=
  .finsupp ..

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

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

Разделы

Аффилиация

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