compLinearMap_inj — Mathlib

English

Let f be a surjective linear map; then the map g ↦ g.compLinearMap f is injective on alternating maps.

Русский

Пусть f — сюръективное линейное отображение; тогда отображение g ↦ g.compLinearMap f инъективно на чередующихся отображениях.

LaTeX

$$Surjective f \\Rightarrow (g_1.compLinearMap f = g_2.compLinearMap f \\iff g_1 = g_2)$$

Lean4

theorem compLinearMap_inj (f : M₂ →ₗ[R] M) (hf : Function.Surjective f) (g₁ g₂ : M [⋀^ι]→ₗ[R] N) :
    g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂ :=
  (compLinearMap_injective _ hf).eq_iff

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