instFreeSubtypeMemSubmodule

Mathlib.RingTheory.Polynomial.DegreeLT

URI: https://scilib.ai/kg/mathlib#Polynomial.degreeLT.instFreeSubtypeMemSubmodule

English

Let R be a semiring. The R-module R[X]_n is free, i.e., it has a basis (for example {1, X, ..., X^{n-1}}).

Русский

Пусть R — полускольная кольцо. Модуль R[X]_n над R свободен, т.е. существует базис (например {1, X, ..., X^{n-1}}).

LaTeX

$$$R[X]_n \\text{ is a free } R\\text{-module with basis } \\{1, X, \\ldots, X^{n-1}\\}. $$$

Lean4

instance : Module.Free R R[X]_n :=
  .of_basis <| basis ..

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

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

Разделы

Аффилиация

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