injective_linearMapComp_right — Mathlib

English

If g is surjective, then the map f ↦ f ∘ g is injective on linear maps; i.e., f ∘ g = f' ∘ g implies f = f'.

Русский

Если g сюръективен, то отображение f ↦ f ∘ g инъективно на линейных отображениях: f ∘ g = f' ∘ g ⇒ f = f'.

LaTeX

$$$\text{If } \mathrm{Surjective}(g),\; f, f': M_2 \to_{\sigma_{23}} M_3:\; f \circ g = f' \circ g \Rightarrow f = f'.$$$

Lean4

/-- The linear map version of `Function.Surjective.injective_comp_right` -/
theorem _root_.Function.Surjective.injective_linearMapComp_right (hg : Surjective g) :
    Injective fun f : M₂ →ₛₗ[σ₂₃] M₃ ↦ f.comp g := fun _ _ h ↦ ext <| hg.forall.2 (LinearMap.ext_iff.1 h)

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