symm_comp_cancel_left — Mathlib

English

Let e: M1 ≃ M2 and f: M2 ≃ M3. Then e.trans (e.symm.trans f) = f, i.e., inserting an inverse in the middle does nothing.

Русский

Пусть e: M1 ≃ M2 и f: M2 ≃ M3. Тогда e.trans (e.symm.trans f) = f, то есть вставка обратного в середине ничего не меняет.

LaTeX

$$$ e_{12}.trans (e_{12}.symm.trans f) = f $$$

Lean4

theorem symm_comp_cancel_left (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₃ →ₛₗ[σ₃₁] M₁) :
    e.symm.toLinearMap ∘ₛₗ (e.toLinearMap ∘ₛₗ f) = f := by ext; simp

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