comp — Mathlib

English

IsStableUnderBaseChange for FormallySmooth; formal property persists under base change.

Русский

Устойчива к базовому изменению для формально гладкого; свойство сохраняется при базовых изменениях.

LaTeX

$$$\text{IsStableUnderBaseChange}(\mathrm{FormallySmooth})$$$

Lean4

/-- Composition of smooth ring homomorphisms is smooth. -/
theorem comp {f : R →+* S} {g : S →+* T} (hf : f.Smooth) (hg : g.Smooth) : (g.comp f).Smooth :=
  stableUnderComposition f g hf hg

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