ext — Mathlib

English

If two A-linear maps from the tensor product M ⊗R N to P agree on all simple tensors x ⊗ y, then the two maps are equal.

Русский

Пусть две линейные относительно A отображения g,h: M ⊗R N →A P agree на всех простых тензорах x ⊗ y; тогда g = h.

LaTeX

$$$\forall g,h : M \otimes_R N \to_A P,\ (\forall x\in M)(\forall y\in N),\ g(x \otimes_R y) = h(x \otimes_R y) \Rightarrow g = h$$$

Lean4

theorem ext {g h : M ⊗[R] N →ₗ[A] P} (H : ∀ x y, g (x ⊗ₜ y) = h (x ⊗ₜ y)) : g = h :=
  curry_injective <| LinearMap.ext₂ H

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