free_asModule_free — Mathlib

English

The representation (Representation.free k G α).asModule is a free module over the algebra MonoidAlgebra k G.

Русский

Репрезентация (Representation.free k G α).asModule является свободным модулем над алгеброй MonoidAlgebra k G.

LaTeX

$$$\text{Module.Free}\bigl(\operatorname{MonoidAlgebra} \ k \ G,\ (\mathrm{Representation.free}\ k\ G\ \alpha).\mathrm{asModule}\bigr)$$$

Lean4

theorem free_asModule_free : Module.Free (MonoidAlgebra k G) (free k G α).asModule :=
  Module.Free.of_basis (freeAsModuleBasis k G α)

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