eq_comp_toLinearMap_symm — Mathlib

English

Let e12: M1 ≃ M2 be a linear equivalence, and f: M3 → M? and g: M1 → M3 be linear maps. Then f = g ∘ e12^{-1} iff f ∘ e12 = g.

Русский

Пусть e12: M1 ≃ M2 — линейное эквивалентность, f: M3 → M? и g: M1 → M3 — линейные отображения. Тогда f = g ∘ e12^{-1} тогда и только тогда, когда f ∘ e12 = g.

LaTeX

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

Lean4

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

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