mapEquiv_symm — Mathlib

English

For any algebra equivalence e, the inverse map of mapAlgEquiv σ e equals mapAlgEquiv σ e.symm.

Русский

Для любой эквивалентности A₁ ≃ₐ[R] A₂ обратное отображение mapAlgEquiv σ e равно mapAlgEquiv σ e.symm.

LaTeX

$$$$ (mapAlgEquiv \\; σ\\; e)^{-1} = mapAlgEquiv \\; σ\\; e^{-1}. $$$$

Lean4

@[simp]
theorem mapEquiv_symm [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) : (mapEquiv σ e).symm = mapEquiv σ e.symm :=
  rfl

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