English
The graded multiplication by the unit 1 acts as the identity: cast (zero_add n) (ₜ1 ₜ* a) = a for any a ∈ ⨂^n M, and similarly for sums.
Русский
Умножение единицей 1 по градуированному умножению является тождественным: cast (zero_add n) (ₜ1 ₜ* a) = a и аналогично для сумм.
LaTeX
$$cast R M (zero_add n) (ₜ1 ₜ* a) = a$$
Lean4
theorem one_mul {n} (a : ⨂[R]^n M) : cast R M (zero_add n) (ₜ1 ₜ* a) = a :=
by
rw [gMul_def, gOne_def]
induction a using PiTensorProduct.induction_on with
| smul_tprod r
a =>
rw [TensorProduct.tmul_smul, LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def, tprod_mul_tprod, cast_tprod]
congr 2 with i
rw [Fin.elim0_append]
refine congr_arg a (Fin.ext ?_)
simp
| add x y hx hy => rw [TensorProduct.tmul_add, map_add, map_add, hx, hy]
