function — Mathlib

English

The product of free modules indexed by a finite set is free in the non-dependent sense.

Русский

Произведение свободных модулей, индексируемое конечным множеством, свободно в нередуцированном виде.

LaTeX

$$$\text{Module.Free.function}$: $\forall ι$ finite, if each $M_i$ is free then $\prod_{i\in ι} M_i$ is free.$$

Lean4

/-- The product of finitely many free modules is free (non-dependent version to help with typeclass
search). -/
instance _root_.Module.Free.function [Finite ι] [Module.Free R M] : Module.Free R (ι → M) :=
  Free.pi _ _

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