tensor_ext₃' — Mathlib

English

Let f,g: (M1 ⊗ M2) ⊗ M3 ⟶ M4 be morphisms with f(m1 ⊗ m2 ⊗ m3) = g(m1 ⊗ m2 ⊗ m3) for all m1,m2,m3; then f = g.

Русский

Пусть f,g: (M1 ⊗ M2) ⊗ M3 ⟶ M4 — гомоморфизмы, удовлетворяющие f(m1 ⊗ m2 ⊗ m3) = g(m1 ⊗ m2 ⊗ m3) для всех m_i; тогда f = g.

LaTeX

$$$\\forall m_1,m_2,m_3:\\; f(m_1 \\otimes m_2 \\otimes m_3) = g(m_1 \\otimes m_2 \\otimes m_3) \\Rightarrow f = g$$$

Lean4

/-- Extensionality lemma for morphisms from a module of the form `(M₁ ⊗ M₂) ⊗ M₃`. -/
theorem tensor_ext₃' {f g : (M₁ ⊗ M₂) ⊗ M₃ ⟶ M₄} (h : ∀ m₁ m₂ m₃, f (m₁ ⊗ₜ m₂ ⊗ₜ m₃) = g (m₁ ⊗ₜ m₂ ⊗ₜ m₃)) : f = g :=
  hom_ext <| TensorProduct.ext_threefold h

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