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 _ _