algEquivOfAlgEquiv_mk' — Mathlib

English

The image of mk' under algEquivOfAlgEquiv coincides with mk' on the target localization.

Русский

Образ mk' под algEquivOfAlgEquiv совпадает с mk' на целевой локализации.

LaTeX

$$$\\mathrm{algEquivOfAlgEquiv}(S,Q,h,H)(\\mathrm{mk'}_S x y) = \\mathrm{mk'}_Q(h x) \\langle h y, \\dots \\rangle$$$

Lean4

theorem algEquivOfAlgEquiv_mk' (x : R) (y : M) :
    algEquivOfAlgEquiv S Q h H (mk' S x y) = mk' Q (h x) ⟨h y, show h y ∈ T from H ▸ Set.mem_image_of_mem h y.2⟩ := by
  simp [map_mk']

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