dfinsupp — Mathlib

English

If each M i is a free R-module, then the DFinsupp space Π₀ i, M_i is a free R-module, with a basis given by the construction DFinsupp.basis.

Русский

Если каждый M_i свободен как модуль над R, то DFinsupp-пространство Π₀ i, M_i свободно над R, и его база задаётся конструкцией DFinsupp.basis.

LaTeX

$$$\\text{Module.Free } R\\left(\\Pi_{0} i, M_i\\right)$$$

Lean4

instance _root_.Module.Free.dfinsupp [∀ i : ι, Module.Free R (M i)] : Module.Free R (Π₀ i, M i) :=
  .of_basis <| DFinsupp.basis fun i => Module.Free.chooseBasis R (M i)

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