Formal-unramification of finite products of rings

Main result

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

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

instance Algebra.FormallyUnramified.instForall {R : Type (max u v)} {I : Type v} [Finite I] (f : I → Type (max u v)) [CommRing R] [(i : I) → CommRing (f i)] [(i : I) → Algebra R (f i)] [∀ (i : I), FormallyUnramified R (f i)] : FormallyUnramified R ((i : I) → f i)