isStandardSmooth_respectsIso — Mathlib

English

IsStandardSmooth respects isomorphisms: it is preserved under ring isomorphisms.

Русский

IsStandardSmooth сохраняется под изоморфизмами колец: гладкость сохраняется при изоморфизмах колец.

LaTeX

$$$$ \operatorname{RespectsIso}(\operatorname{IsStandardSmooth}). $$$$

Lean4

theorem isStandardSmooth_respectsIso : RespectsIso @IsStandardSmooth :=
  by
  apply isStandardSmooth_stableUnderComposition.respectsIso
  introv
  exact (IsStandardSmoothOfRelativeDimension.equiv e).isStandardSmooth

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