comp_symm — Mathlib

English

The composition of the map e with its inverse is the identity on the codomain: e ∘ e.symm = id on A₂.

Русский

Составление мапы e с ее обратной даёт тождественный отображение на целевом множестве.

LaTeX

$$$\text{AlgHom}.comp(e, e^{-1}) = \mathrm{id}$$$

Lean4

@[simp]
theorem comp_symm (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp (e : A₁ →ₐ[R] A₂) ↑e.symm = AlgHom.id R A₂ :=
  by
  ext
  simp

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