eq_comp_toLinearMap_iff — Mathlib

English

Let e12: M1 ≃ M2. For any f,g: M3 → M1, equality e12.toLinearMap ∘ f = e12.toLinearMap ∘ g holds iff f = g.

Русский

Пусть e12: M1 ≃ M2. Пусть f,g: M3 → M1. Равенство e12.toLinearMap ∘ f = e12.toLinearMap ∘ g эквивалентно f = g.

LaTeX

$$$ e_{12}.toLinearMap \circ f = e_{12}.toLinearMap \circ g \;\Longleftrightarrow\; f = g $$$

Lean4

@[simp]
theorem eq_comp_toLinearMap_iff (f g : M₂ →ₛₗ[σ₂₃] M₃) : f.comp e₁₂.toLinearMap = g.comp e₁₂.toLinearMap ↔ f = g :=
  by
  refine ⟨fun h => ?_, fun a ↦ congrFun (congrArg LinearMap.comp a) e₁₂.toLinearMap⟩
  rw [(eq_comp_toLinearMap_symm g (f.comp e₁₂.toLinearMap)).mpr h.symm, eq_comp_toLinearMap_symm]

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