English
The product of mk's corresponding to single-vector tensor factors equals mk of the full tprod x.
Русский
Произведение элементов mk, соответствующих одно-элементным тензорным степеням, равно mk тензорного произведения x.
LaTeX
$$$ (List.finRange n).map (\(a) => (GradedMonoid.mk 1 (MultilinearMap.instFunLikeForall.coe (PiTensorProduct.tprod R) (fun x_1 => x a)))) .prod = GradedMonoid.mk n (MultilinearMap.instFunLikeForall.coe (PiTensorProduct.tprod R) x) $$$
Lean4
/-- The product of tensor products made of a single vector is the same as a single product of
all the vectors. -/
theorem _root_.TensorPower.list_prod_gradedMonoid_mk_single (n : ℕ) (x : Fin n → M) :
((List.finRange n).map fun a =>
(GradedMonoid.mk _ (PiTensorProduct.tprod R fun _ : Fin 1 => x a) : GradedMonoid fun n => ⨂[R]^n M)).prod =
GradedMonoid.mk n (PiTensorProduct.tprod R x) :=
by
refine Fin.consInduction ?_ ?_ x <;> clear x
· rw [List.finRange_zero, List.map_nil, List.prod_nil]
rfl
· intro n x₀ x ih
rw [List.finRange_succ_eq_map, List.map_cons, List.prod_cons, List.map_map]
simp_rw [Function.comp_def, Fin.cons_zero, Fin.cons_succ]
rw [ih, GradedMonoid.mk_mul_mk, TensorPower.tprod_mul_tprod]
refine TensorPower.gradedMonoid_eq_of_cast (add_comm _ _) ?_
dsimp only [GradedMonoid.mk]
rw [TensorPower.cast_tprod]
simp_rw [Fin.append_left_eq_cons, Function.comp_def]
congr 1 with i