Theorems · Theorem · commutative algebra

Algebra.FormallySmooth.of_pi

∀ {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)] [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 130 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraAlgebra.FormallySmooth