Formal-étaleness of finite products of rings

Main result

• Algebra.FormallyEtale.pi_iff: If I is finite, Π i : I, A i is R-formally-étale if and only if each A i is R-formally-étale.

theorem Algebra.FormallyEtale.pi_iff {R : Type (max u v)} {I : Type u} (A : I → Type (max u v)) [CommRing R] [(i : I) → CommRing (A i)] [(i : I) → Algebra R (A i)] [Finite I] : Algebra.FormallyEtale R ((i : I) → A i) ↔ ∀ (i : I), Algebra.FormallyEtale R (A i)

instance Algebra.FormallyEtale.instForallOfFinite {R : Type (max u v)} {I : Type u} (A : I → Type (max u v)) [CommRing R] [(i : I) → CommRing (A i)] [(i : I) → Algebra R (A i)] [Finite I] [∀ (i : I), Algebra.FormallyEtale R (A i)] : Algebra.FormallyEtale R ((i : I) → A i)