English
The class of standard-smooth maps is closed under composition: if f: R →+* S and g: S →+* T are standard-smooth, then g ∘ f: R →+* T is standard-smooth.
Русский
Класс стандартно гладких отображений замкнут относительно композиции: если f: R →+* S и g: S →+* T гладкие, то g ∘ f: R →+* T гладко.
LaTeX
$$$$ \forall R S T [\mathrm{CommRing} R] [\mathrm{CommRing} S] [\mathrm{CommRing} T](f : R \to+* S)(g : S \to+* T), \; \operatorname{IsStandardSmooth}(f) \to \operatorname{IsStandardSmooth}(g) \to \operatorname{IsStandardSmooth}(g \circ f). $$$$
Lean4
theorem comp {g : S →+* T} {f : R →+* S} (hg : IsStandardSmooth g) (hf : IsStandardSmooth f) :
IsStandardSmooth (g.comp f) := by
rw [IsStandardSmooth]
algebraize [f, g, (g.comp f)]
exact Algebra.IsStandardSmooth.trans R S T
