English
If each M_i is finitely presented, then the product space ∏_i M_i is finitely presented (for finite index set ι).
Русский
Если каждый M_i конечнопредставим, то продуктовый простор ∏_i M_i конечнопредставим (при конечном индексе ι).
LaTeX
$$$[\forall i, Module.FinitePresentation R (M i)] \Rightarrow Module.FinitePresentation R ((i : \mathcal{I}) \to M i)$$$
Lean4
instance pi {ι : Type*} (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
[∀ i, Module.FinitePresentation R (M i)] [Finite ι] : Module.FinitePresentation R (∀ i, M i) :=
by
refine
Module.pi_induction' (motive := fun N _ _ ↦ Module.FinitePresentation R N) (motive' := fun N _ _ ↦
Module.FinitePresentation R N) R ?_ ?_ ?_ ?_ M inferInstance
· exact fun e (hN : Module.FinitePresentation _ _) ↦ .of_equiv e
· exact fun e (hN : Module.FinitePresentation _ _) ↦ .of_equiv e
· infer_instance
· introv hN hN'
infer_instance
