instForallOfFinite — Mathlib

English

If I is a finite index set and each A_i is a formally étale R-algebra, then the product algebra ∏_i A_i is also formally étale over R. This is a standard stability under finite product for étale algebras.

Русский

Если множество индексов I конечно, и каждый A_i является формально этиальной R-алгеброй, то произведение ∏_i A_i также формально этиально над R. Это свойство стабильности по конечному произведению для этиальных алгебр.

LaTeX

$$$\\text{Finite}(I) \\Rightarrow (\\forall i, \\text{FormallyEtale } R (A_i)) \\Rightarrow \\text{FormallyEtale } R (\\Pi_{i\\in I} A_i)$$$

Lean4

instance [Finite I] [∀ i, FormallyEtale R (A i)] : FormallyEtale R (Π i, A i) :=
  .of_unramified_and_smooth

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