English
The product of finitely many free modules is free.
Русский
Произведение конечного числа свободных модулей свободно.
LaTeX
$$$\text{Module.Free } R (\forall i, M_i)$ is free when each M_i is free and the index set is finite: $(\forall i, \text{Module.Free } R (M_i)) \Rightarrow \text{Module.Free } R (\forall i, M_i)$.$$
Lean4
/-- The product of finitely many free modules is free. -/
instance _root_.Module.Free.pi (M : ι → Type*) [Finite ι] [∀ i : ι, AddCommMonoid (M i)] [∀ i : ι, Module R (M i)]
[∀ i : ι, Module.Free R (M i)] : Module.Free R (∀ i, M i) :=
let ⟨_⟩ := nonempty_fintype ι
.of_basis <| Pi.basis fun i => Module.Free.chooseBasis R (M i)
