comp — Mathlib

English

Étale is stable under composition: if R → A and A → B are étale then R → B is étale.

Русский

Étale сохраняется при композиции: если R → A и A → B étale, то R → B étale.

LaTeX

$$$[\text{Algebra } R A]\,[{\text{Algebra } A B}]\,[\text{Etale } R A]\,[\text{Etale } A B]\Rightarrow \text{Etale } R B$$$

Lean4

theorem comp [FormallyEtale R A] [FormallyEtale A B] : FormallyEtale R B :=
  FormallyEtale.iff_unramified_and_smooth.mpr ⟨FormallyUnramified.comp R A B, FormallySmooth.comp R A B⟩

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