comp_toLinearMap_eq_iff — Mathlib

English

If f: M3 → M1 and g: M3 → M2 satisfy f = e12.symm ∘ 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

@[simp]
theorem comp_toLinearMap_eq_iff (f g : M₃ →ₛₗ[σ₃₁] M₁) : e₁₂.toLinearMap.comp f = e₁₂.toLinearMap.comp g ↔ f = g :=
  by
  refine ⟨fun h => ?_, congrArg e₁₂.comp⟩
  rw [← (toLinearMap_symm_comp_eq g (e₁₂.toLinearMap.comp f)).mpr h, eq_toLinearMap_symm_comp]

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