Algebra.FormallyEtale.iff_unramified_and_smooth

theorem Algebra.FormallyEtale.iff_unramified_and_smooth : ∀ {R : Type u} [inst : CommSemiring R] {A : Type u} [inst_1 : Semiring A] [inst_2 : Algebra R A], Algebra.FormallyEtale R A ↔ Algebra.FormallyUnramified R A ∧ Algebra.FormallySmooth R A

This theorem states that for any commutative semiring R and any semiring A that is an algebra over R, A is formally etale (i.e., it satisfies certain smoothness and flatness conditions) if and only if A is both formally unramified (i.e., all of its derivations are trivial) and formally smooth (i.e., it can be locally deformed into a regular ring).

More concisely: A commutative semiring A, which is an algebra over a commutative semiring R, is formally etale if and only if it is both formally unramified and formally smooth.