mapEquiv_symm — Mathlib

English

For any monoid isomorphism h, the inverse of the induced units equivalence equals the induced units equivalence of the inverse, i.e., (mapEquiv h)^{-1} = mapEquiv (h^{-1}).

Русский

Для любого изоморфизма моноидов h обратимый эквивалент единиц удовлетворяет (mapEquiv(h))^{-1} = mapEquiv(h^{-1}).

LaTeX

$$$(\\mathrm{mapEquiv}(h))^{-1} = \\mathrm{mapEquiv}(h^{-1})$$$

Lean4

@[simp]
theorem mapEquiv_symm (h : M ≃* N) : (mapEquiv h).symm = mapEquiv h.symm :=
  rfl

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