instFree

Mathlib.RingTheory.MvPolynomial.Basic

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

← MathLib Explorer

English

The R-module MvPolynomial σ R is free.

Русский

Модуль MvPolynomial(σ,R) над R свободен.

LaTeX

$$$\\text{Module.Free}\\; R\\; (\\mathrm{MvPolynomial}(σ,R))$$$

Lean4

/-- The `R`-module `MvPolynomial σ R` is free. -/
instance : Module.Free R (MvPolynomial σ R) :=
  Module.Free.of_basis (MvPolynomial.basisMonomials σ R)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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