of_unramified_and_smooth — Mathlib

English

If a morphism is formally unramified and formally smooth, then it is formally étale.

Русский

Если отображение формально нерасчленимо и формально гладко, то оно формально étale.

LaTeX

$$$\text{FormallyUnramified}(R,A) \land \text{FormallySmooth}(R,A) \Rightarrow \text{FormallyEtale}(R,A)$$$

Lean4

theorem of_unramified_and_smooth [h₁ : FormallyUnramified R A] [h₂ : FormallySmooth R A] : FormallyEtale R A :=
  FormallyEtale.iff_unramified_and_smooth.mpr ⟨h₁, h₂⟩

Похожие утверждения