comp — Mathlib

English

If R → A is formally étale, then it is formally smooth.

Русский

Если R → A формально étale, то оно формально гладкое.

LaTeX

$$$[h : FormallyEtale\; R\; A] \Rightarrow [FormallySmooth\; R\; A]$$$

Lean4

/-- Étale is stable under composition. -/
theorem comp [Algebra A B] [IsScalarTower R A B] [Etale R A] [Etale A B] : Etale R B
    where
  formallyEtale := FormallyEtale.comp R A B
  finitePresentation := FinitePresentation.trans R A B

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