ringEquivOfRingEquiv_mk' — Mathlib

English

Under the localization isomorphism, mk' maps to mk' in the target, with the numerator mapped by j and the denominator mapped to an element of T.

Русский

Под изоморфизмом локализации mk' отображается в mk' целевой локализации, где числитель перенесён через j, а знаменатель отображается в элемент T.

LaTeX

$$$$ \\mathrm{ringEquivOfRingEquiv}(S,Q,j,H)(\\mathrm{mk}' S x y) = \\mathrm{mk}' Q (j x) \\langle j y, \\text{proof} \\rangle $$$$

Lean4

theorem ringEquivOfRingEquiv_mk' {j : R ≃+* P} (H : M.map j.toMonoidHom = T) (x : R) (y : M) :
    ringEquivOfRingEquiv S Q j H (mk' S x y) = mk' Q (j x) ⟨j y, show j y ∈ T from H ▸ Set.mem_image_of_mem j y.2⟩ := by
  simp [map_mk']

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