comp_toLinearMap_symm_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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