isSmooth_isStableUnderBaseChange — Mathlib

English

Smoothness is stable under base change.

Русский

Гладкость сохраняется при базовом изменении.

LaTeX

$$isSmooth_isStableUnderBaseChange$$

Lean4

/-- Smooth of relative dimension `n` is stable under base change. -/
theorem isSmooth_isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @IsSmooth :=
  HasRingHomProperty.isStableUnderBaseChange <|
    locally_isStableUnderBaseChange isStandardSmooth_respectsIso isStandardSmooth_isStableUnderBaseChange

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