injective_linearMapComp_left — Mathlib

English

For semilinear maps f, g, h, the equality ((h ∘ g) ∘ f) = (h ∘ (g ∘ f)) holds (associativity of composition).

Русский

Для полилинейных отображений f, g, h верно (h ∘ g) ∘ f = h ∘ (g ∘ f) (ассоциативность композиции).

LaTeX

$$$((h \circ g) \circ f) = (h \circ (g \circ f)).$$$

Lean4

/-- The linear map version of `Function.Injective.comp_left` -/
theorem _root_.Function.Injective.injective_linearMapComp_left (hf : Injective f) :
    Injective fun g : M₁ →ₛₗ[σ₁₂] M₂ ↦ f.comp g := fun g₁ g₂ (h : f.comp g₁ = f.comp g₂) ↦
  ext fun x ↦ hf <| by rw [← comp_apply, h, comp_apply]

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