English
Extensionality principle for PiTensorProduct: φ1 = φ2 if they agree after composing with tprod.
Русский
Принцип эквивалентности для PiTensorProduct: φ1 = φ2, если они совпадают после композиции с tprod.
LaTeX
$$$$ \phi_1 = \phi_2 \text{ if } \phi_1 \circ tprod = \phi_2 \circ tprod $$$$
Lean4
@[ext]
theorem ext {φ₁ φ₂ : (⨂[R] i, s i) →ₗ[R] E} (H : φ₁.compMultilinearMap (tprod R) = φ₂.compMultilinearMap (tprod R)) :
φ₁ = φ₂ := by
refine LinearMap.ext ?_
refine fun z ↦ PiTensorProduct.induction_on' z ?_ fun {x y} hx hy ↦ by rw [φ₁.map_add, φ₂.map_add, hx, hy]
· intro r f
rw [tprodCoeff_eq_smul_tprod, φ₁.map_smul, φ₂.map_smul]
apply congr_arg
exact MultilinearMap.congr_fun H f
