instModuleFree — Mathlib

English

If M is a free R-module, then the tensor algebra on M is a free R-module as well.

Русский

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

LaTeX

$$$ Module.Free R (TensorAlgebra R M) $$$

Lean4

/-- `TensorAlgebra R M` is free when `M` is. -/
instance instModuleFree [Module.Free R M] : Module.Free R (TensorAlgebra R M) :=
  let ⟨⟨_κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  .of_basis b.tensorAlgebra

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