tprod_mul_tprod — Mathlib

English

The product of two homogeneous tprod elements corresponds to tprod over the concatenation of their index lists: tprod_R a ₜ* tprod_R b = tprod_R (Fin.append a b).

Русский

Произведение двух однородных элементов tprod соответствует tprod по конкатенации индексов: tprod_R a ₜ* tprod_R b = tprod_R (Fin.append a b).

LaTeX

$$tprod_R a ₜ* tprod_R b = tprod_R (Fin.append a b)$$

Lean4

theorem tprod_mul_tprod {na nb} (a : Fin na → M) (b : Fin nb → M) : tprod R a ₜ* tprod R b = tprod R (Fin.append a b) :=
  by
  dsimp [gMul_def, mulEquiv]
  rw [tmulEquiv_apply R M a b]
  refine (reindex_tprod _ _).trans ?_
  congr 1
  dsimp only [Fin.append, finSumFinEquiv, Equiv.coe_fn_symm_mk]
  apply funext
  apply Fin.addCases <;> simp

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