eq_toLinearMap_symm_comp — Mathlib

English

If f: M3 → M1 and g: M3 → M2 satisfy f = e12^{-1} ∘ g, then e12 ∘ f = g.

Русский

Пусть f: M3 → M1 и g: M3 → M2 удовлетворяют f = e12^{-1} ∘ g. Тогда e12 ∘ f = g.

LaTeX

$$$ f = e_{12}^{-1} \circ g \;\Longrightarrow\; e_{12} \circ f = g $$$

Lean4

theorem eq_toLinearMap_symm_comp (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
    f = e₁₂.symm.toLinearMap.comp g ↔ e₁₂.toLinearMap.comp f = g :=
  by
  constructor <;> intro H <;> ext
  · simp [H]
  · simp [← H]

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