instModuleFree — Mathlib

English

If M is a free module over R, then SymmetricAlgebra R M is a free R-module as well.

Русский

Если M — свободный модуль над R, то и SymmetricAlgebra R M также свободный R-модуль.

LaTeX

$$$[\text{Module.Free } R M] \Rightarrow [\text{Module.Free } R (\operatorname{Sym}_R M)].$$$

Lean4

/-- `SymmetricAlgebra R M` is free when `M` is. -/
instance instModuleFree [Module.Free R M] : Module.Free R (SymmetricAlgebra R M) :=
  let ⟨⟨_I, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  .of_basis b.symmetricAlgebra

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