instForallOfFinite — Mathlib

English

If finite index set I and each A_i is formally smooth over R, then the product Π_i A_i is formally smooth over R.

Русский

Если индексный набор конечен и каждая A_i формально гладка над R, то произведение Π_i A_i формально гладко над R.

LaTeX

$$$\text{Finite } I \Rightarrow (\forall i, \mathrm{FormallySmooth}(R, A_i)) \Rightarrow \mathrm{FormallySmooth}(R, \prod_i A_i)$$$

Lean4

instance [Finite I] [∀ i, FormallySmooth R (A i)] : FormallySmooth R (Π i, A i) :=
  (pi_iff _).mpr ‹_›

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