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 u_1} {I : Type u_2} (A : I → Type u_3) [CommRing R] [(i : I) → CommRing (A i)] [(i : I) → Algebra R (A i)] [Finite I] : FormallyEtale R ((i : I) → A i) ↔ ∀ (i : I), FormallyEtale R (A i)

instance Algebra.FormallyEtale.instForallOfFinite {R : Type u_1} {I : Type u_2} (A : I → Type u_3) [CommRing R] [(i : I) → CommRing (A i)] [(i : I) → Algebra R (A i)] [Finite I] [∀ (i : I), FormallyEtale R (A i)] : FormallyEtale R ((i : I) → A i)

instance Algebra.FormallyEtale.instEtaleForallOfFinite {R : Type u_1} {I : Type u_2} (A : I → Type u_3) [CommRing R] [(i : I) → CommRing (A i)] [(i : I) → Algebra R (A i)] [Finite I] [∀ (i : I), Etale R (A i)] : Etale R ((i : I) → A i)