list_prod_gradedMonoid_mk_single — Mathlib

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

Похожие утверждения