instFree

Mathlib.LinearAlgebra.Finsupp.VectorSpace

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

English

The MonoidAlgebra S ι is free over R; freeness is inherited from the finsupp construction.

Русский

MonoidAlgebra S ι свободен над R; свобода следует из конструкции через Finsupp.

LaTeX

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

Lean4

instance : Module.Free R (MonoidAlgebra S ι) :=
  .finsupp ..

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

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

Разделы

Аффилиация

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