English
Another structural extensionality principle for a differently nested tensor product.
Русский
Другой принцип экстрансиональности для иначе вложенного тензорного произведения.
LaTeX
$$$\\forall g,h : M \\otimes_R (N \\otimes_R (P \\otimes_R Q)) \\to S,\\ (\\forall m\\in M, n\\in N, p\\in P, q\\in Q), g(m \\otimes (n \\otimes (p \\otimes q))) = h(m \\otimes (n \\otimes (p \\otimes q))) \\Rightarrow g=h$.$$
Lean4
/-- Two linear maps (M ⊗ N) ⊗ (P ⊗ Q) → S which agree on all elements of the
form (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) are equal. -/
theorem ext_fourfold' {φ ψ : M ⊗[R] N ⊗[R] (P ⊗[R] Q) →ₗ[R] S}
(H : ∀ w x y z, φ (w ⊗ₜ x ⊗ₜ (y ⊗ₜ z)) = ψ (w ⊗ₜ x ⊗ₜ (y ⊗ₜ z))) : φ = ψ :=
by
ext m n p q
exact H m n p q