compLinearMap_inj — Mathlib

English

If two multilinear maps become equal after composing with a family of surjective linear maps, then the two maps were equal to begin with.

Русский

Если две мультиленейные карты становятся равными после композиции с сюръективной семейством линейных отображений, то изначально они равны.

LaTeX

$$$ g_1.compLinearMap f = g_2.compLinearMap f \\;\\Rightarrow\\; g_1 = g_2$ (provided surjectivity holds)$$

Lean4

theorem compLinearMap_inj (f : ∀ i, M₁ i →ₗ[R] M₁' i) (hf : ∀ i, Surjective (f i)) (g₁ g₂ : MultilinearMap R M₁' M₂) :
    g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂ :=
  (compLinearMap_injective _ hf).eq_iff

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