Theorems · Theorem · commutative algebra

Algebra.FormallySmooth.pi_iff

∀ {R : Type u_1} {I : Type u_2} (A : I → Type u_3) [inst : CommRing R] [inst_1 : (i : I) → CommRing (A i)]
  [inst_2 : (i : I) → Algebra R (A i)] [Finite I],
  Algebra.FormallySmooth R ((i : I) → A i) ↔ ∀ (i : I), Algebra.FormallySmooth R (A i)

Defined in

Mathlib.RingTheory.Smooth.Pi

Cited by

1 results in Mathlib

Foundations

Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraFinite