ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
⊢ ∀ (x : ⨂[R] (i : ι), s i), ↑φ₁ x = ↑φ₂ x
ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
⊢ φ₁ = φ₂
refine' LinearMap.ext _
ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
⊢ ∀ {r : R} {f : (i : ι) → s i}, ↑φ₁ (tprodCoeff R r f) = ↑φ₂ (tprodCoeff R r f)
ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
⊢ ∀ (x : ⨂[R] (i : ι), s i), ↑φ₁ x = ↑φ₂ x
refine' fun z ↦
  PiTensorProduct.induction_on' z _ fun {x y} hx hy ↦ by rw [φ₁.map_add, φ₂.map_add, hx, hy]
no goals
ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z x y : ⨂[R] (i : ι), s i
hx : ↑φ₁ x = ↑φ₂ x
hy : ↑φ₁ y = ↑φ₂ y
⊢ ↑φ₁ (x + y) = ↑φ₂ (x + y)
rw [φ₁.map_add, φ₂.map_add, hx, hy]
ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ ↑φ₁ (tprodCoeff R r f) = ↑φ₂ (tprodCoeff R r f)
ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
⊢ ∀ {r : R} {f : (i : ι) → s i}, ↑φ₁ (tprodCoeff R r f) = ↑φ₂ (tprodCoeff R r f)
intro r f
ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ r • ↑φ₁ (↑(tprod R) f) = r • ↑φ₂ (↑(tprod R) f)
ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ ↑φ₁ (tprodCoeff R r f) = ↑φ₂ (tprodCoeff R r f)
rw [tprodCoeff_eq_smul_tprod, φ₁.map_smul, φ₂.map_smul]
case h
ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ ↑φ₁ (↑(tprod R) f) = ↑φ₂ (↑(tprod R) f)
ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ r • ↑φ₁ (↑(tprod R) f) = r • ↑φ₂ (↑(tprod R) f)
apply _root_.congr_arg
no goals
case h
ι : Type u_3
ι₂ : Type ?u.234224
ι₃ : Type ?u.234227
R : Type u_1
inst✝⁷ : CommSemiring R
R₁ : Type ?u.234236
R₂ : Type ?u.234239
s : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.234429
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_4
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.234697
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ ↑φ₁ (↑(tprod R) f) = ↑φ₂ (↑(tprod R) f)
exact MultilinearMap.congr_fun H f