English
The tensor powers ⨂[R]^i M form a graded semiring under the graded multiplication gMul, with natural embeddings and structure maps respecting the grading.
Русский
Тензорные степени ⨂[R]^i M образуют градуированную полугруппу с естественным градуированием и структурными отображениями, согласованными с градацией.
LaTeX
$$$ DirectSum.GSemiring\\; (i \\mapsto ⨂[R]^i M) $$$
Lean4
instance gsemiring : DirectSum.GSemiring fun i => ⨂[R]^i M :=
{ TensorPower.gmonoid with
mul_zero := fun _ => LinearMap.map_zero _
zero_mul := fun _ => LinearMap.map_zero₂ _ _
mul_add := fun _ _ _ => LinearMap.map_add _ _ _
add_mul := fun _ _ _ => LinearMap.map_add₂ _ _ _ _
natCast := fun n => algebraMap₀ (n : R)
natCast_zero := by simp only [Nat.cast_zero, map_zero]
natCast_succ := fun n => by simp only [Nat.cast_succ, map_add, algebraMap₀_one] }
