free_adjoinRoot — Mathlib

English

If f is monic, then Polynomial.Monic.free_adjoinRoot asserts that AdjoinRoot g is a free module of finite rank over R with basis given by powerBasis'.

Русский

Если g моничный, то AdjoinRoot g — свободная модуль над R конечной ранги с базисом powerBasis'.

LaTeX

$$Module.Free R (AdjoinRoot g) holds if g is Monic$$

Lean4

theorem _root_.Polynomial.Monic.free_adjoinRoot (hg : g.Monic) : Module.Free R (AdjoinRoot g) :=
  .of_basis (powerBasis' hg).basis

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