algEquiv_symm_mk — Mathlib

English

The inverse image under algEquiv M S of the canonical mk' S x y is mk x y in Localization M.

Русский

Образ обратного отображения через algEquiv M S канонического mk' S x y равен mk x y в Localization M.

LaTeX

$$$(\text{algEquiv } M S).\text{symm} (\text{mk}' S x y) = \text{mk} x y$$$

Lean4

theorem algEquiv_symm_mk (x : R) (y : M) : (algEquiv M S).symm (mk' S x y) = mk x y := by
  rw [mk_eq_mk', algEquiv_symm_mk']

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