respectsIso — Mathlib

English

Formally smooth morphisms respect isomorphisms; i.e., the property is invariant under isomorphisms of rings.

Русский

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

LaTeX

$$$\mathrm{RespectsIso}(\mathrm{FormallySmooth})$$$

Lean4

theorem respectsIso : RespectsIso @FormallySmooth :=
  stableUnderComposition.respectsIso fun e ↦ holdsForLocalizationAway.of_bijective _ _ e.bijective

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