Formal-smoothness of finite products of rings

Main result

• Algebra.FormallySmooth.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.FormallySmooth.of_pi {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)] [FormallySmooth R ((i : I) → A i)] (i : I) : FormallySmooth R (A i)

theorem Algebra.FormallySmooth.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] : FormallySmooth R ((i : I) → A i) ↔ ∀ (i : I), FormallySmooth R (A i)

instance Algebra.FormallySmooth.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), FormallySmooth R (A i)] : FormallySmooth R ((i : I) → A i)