tensor_ext — Mathlib

English

If f,g: M1 ⊗ M2 ⟶ M3 are morphisms such that f(m ⊗ n) = g(m ⊗ n) for all m ∈ M1, n ∈ M2, then f = g.

Русский

Если две гомоморфные отображения f,g: M1 ⊗ M2 ⟶ M3 совпадают на всех простых тензорных произведениях m ⊗ n, то они равны.

LaTeX

$$$\\forall m \\in M_1, \\forall n \\in M_2:\\; f(m \\otimes n) = g(m \\otimes n) \\Rightarrow f = g$$$

Lean4

theorem tensor_ext {f g : M₁ ⊗ M₂ ⟶ M₃} (h : ∀ m n, f.hom (m ⊗ₜ n) = g.hom (m ⊗ₜ n)) : f = g :=
  hom_ext <| TensorProduct.ext (by ext; apply h)

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