instFree

Mathlib.LinearAlgebra.Finsupp.VectorSpace

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

English

The polynomial ring R[X] is a free R-module, via the fin-supp representation; the isomorphism to finsupp gives a basis.

Русский

Модуль полиномов R[X] свободен над R; изоморфизм с Finsupp задаёт базис.

LaTeX

$$$\\text{Module.Free } R (R[X])$$$

Lean4

instance : Module.Free R R[X] :=
  .of_equiv (Polynomial.toFinsuppIsoLinear _).symm

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

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

Разделы

Аффилиация

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