English
Composition of two casts equals a single cast along the transitive composition of the indices.
Русский
Состав двух casts равен одному cast по транзитивной композиции индексов.
LaTeX
$${i j k} (h : i = j) (h' : j = k) (a : ⨂^i M) : cast R M h' (cast R M h a) = cast R M (h.trans h') a$$
Lean4
theorem mul_one {n} (a : ⨂[R]^n M) : cast R M (add_zero _) (a ₜ* ₜ1) = a :=
by
rw [gMul_def, gOne_def]
induction a using PiTensorProduct.induction_on with
| smul_tprod r
a =>
rw [← TensorProduct.smul_tmul', LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def, tprod_mul_tprod R a _,
cast_tprod]
congr 2 with i
rw [Fin.append_elim0]
refine congr_arg a (Fin.ext ?_)
simp
| add x y hx hy => rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]
