coe_symm_comp_coe — Mathlib

English

The inverse on the left composed with the forward map on the right yields the identity: (e.symm : M2 →SL[σ₂₁] M1) ∘ (e : M1 →SL[σ₁₂] M2) = id.

Русский

Левополная композиция обратного отображения с прямым отображением даёт тождество: (e.symm) ∘ e = id.

LaTeX

$$$ (e^{-1} : M_2 \\toSL[\\sigma_{21}] M_1) \\circ (e : M_1 \\toSL[\\sigma_{12}] M_2) = \\mathrm{id} $$$

Lean4

@[simp high]
theorem coe_symm_comp_coe (e : M₁ ≃SL[σ₁₂] M₂) :
    (e.symm : M₂ →SL[σ₂₁] M₁).comp (e : M₁ →SL[σ₁₂] M₂) = ContinuousLinearMap.id R₁ M₁ :=
  ContinuousLinearMap.ext e.symm_apply_apply

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