algEquiv — Mathlib

English

Compatibility of the mk' construction with AlgEquiv: applying algEquiv to mk' S x y yields mk' Q (h x) y'

Русский

Совместимость конструкции mk' с AlgEquiv: применение algEquiv к mk' S x y даёт mk' Q (h x) y'.

LaTeX

$$$\\mathrm{algEquiv}\\, (\\mathrm{mk'}(S, x, y)) = \\mathrm{mk'}(Q, h(x), y')$$$

Lean4

/-- If `S`, `Q` are localizations of `R` at the submonoid `M` respectively,
there is an isomorphism of localizations `S ≃ₐ[R] Q`. -/
@[simps!]
noncomputable def algEquiv : S ≃ₐ[R] Q :=
  { ringEquivOfRingEquiv S Q (RingEquiv.refl R) M.map_id with commutes' := ringEquivOfRingEquiv_eq _ }

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