case a
ι : Type u_1
ι₂ : Type ?u.505120
ι₃ : Type ?u.505123
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.505132
R₂ : Type ?u.505135
s : ι → Type ?u.505140
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.505459
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.505593
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ ↑(reindex R M (Equiv.refl ι)) = ↑(LinearEquiv.refl R (⨂[R] (x : ι), M))
ι : Type u_1
ι₂ : Type ?u.505120
ι₃ : Type ?u.505123
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.505132
R₂ : Type ?u.505135
s : ι → Type ?u.505140
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.505459
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.505593
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ reindex R M (Equiv.refl ι) = LinearEquiv.refl R (⨂[R] (x : ι), M)
apply LinearEquiv.toLinearMap_injective
case a
ι : Type u_1
ι₂ : Type ?u.505120
ι₃ : Type ?u.505123
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.505132
R₂ : Type ?u.505135
s : ι → Type ?u.505140
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.505459
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.505593
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ LinearMap.compMultilinearMap (↑(reindex R M (Equiv.refl ι))) (tprod R) =
    LinearMap.compMultilinearMap (↑(LinearEquiv.refl R (⨂[R] (x : ι), M))) (tprod R)
case a
ι : Type u_1
ι₂ : Type ?u.505120
ι₃ : Type ?u.505123
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.505132
R₂ : Type ?u.505135
s : ι → Type ?u.505140
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.505459
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.505593
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ ↑(reindex R M (Equiv.refl ι)) = ↑(LinearEquiv.refl R (⨂[R] (x : ι), M))
refine ext ?_
case a
ι : Type u_1
ι₂ : Type ?u.505120
ι₃ : Type ?u.505123
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.505132
R₂ : Type ?u.505135
s : ι → Type ?u.505140
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.505459
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.505593
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ domDomCongr (Equiv.refl ι) (tprod R) = LinearMap.compMultilinearMap LinearMap.id (tprod R)
case a
ι : Type u_1
ι₂ : Type ?u.505120
ι₃ : Type ?u.505123
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.505132
R₂ : Type ?u.505135
s : ι → Type ?u.505140
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.505459
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.505593
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ LinearMap.compMultilinearMap (↑(reindex R M (Equiv.refl ι))) (tprod R) =
    LinearMap.compMultilinearMap (↑(LinearEquiv.refl R (⨂[R] (x : ι), M))) (tprod R)
rw [reindex_comp_tprod, LinearEquiv.refl_toLinearMap, Equiv.refl_symm]
no goals
case a
ι : Type u_1
ι₂ : Type ?u.505120
ι₃ : Type ?u.505123
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.505132
R₂ : Type ?u.505135
s : ι → Type ?u.505140
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.505459
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.505593
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ domDomCongr (Equiv.refl ι) (tprod R) = LinearMap.compMultilinearMap LinearMap.id (tprod R)
rfl