coe_comp_coe_symm — Mathlib

English

The forward map composed with its inverse is the identity: e.toContinuousAlgHom ∘ e.symm = id_B.

Русский

Прямая карта, композиция с обратной дает тождество: e.toContinuousAlgHom ∘ e.symm = id_B.

LaTeX

$$$e^{\mathrm{toContinuousAlgHom}} \circ e^{-1} = \mathrm{id}_B$$$

Lean4

@[simp high]
theorem coe_comp_coe_symm (e : A ≃A[R] B) : e.toContinuousAlgHom.comp e.symm = ContinuousAlgHom.id R B :=
  ContinuousAlgHom.ext e.apply_symm_apply

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