toLinearMap_symm_comp_eq — Mathlib

English

Let 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 toLinearMap_symm_comp_eq (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
    e₁₂.symm.toLinearMap.comp g = f ↔ g = e₁₂.toLinearMap.comp f :=
  by
  constructor <;> intro H <;> ext
  · simp [← H]
  · simp [H]

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