English
Multiplication is preserved by the DirectSum translation: the direct sum of f * g corresponds to the product of their direct sums.
Русский
Умножение сохраняется через прямое суммирование: прямой сумма f * g соответствует произведению их DirectSum-образов.
LaTeX
$$(f * g).toDirectSum = f.toDirectSum * g.toDirectSum$$
Lean4
@[simp]
theorem toDirectSum_mul [DecidableEq ι] [AddMonoid ι] [Semiring M] (f g : AddMonoidAlgebra M ι) :
(f * g).toDirectSum = f.toDirectSum * g.toDirectSum :=
by
let to_hom : AddMonoidAlgebra M ι →+ ⨁ _ : ι, M :=
{ toFun := toDirectSum
map_zero' := toDirectSum_zero
map_add' := toDirectSum_add }
change to_hom (f * g) = to_hom f * to_hom g
revert f g
rw [AddMonoidHom.map_mul_iff]
ext xi xv yi yv : 4
simp [to_hom, AddMonoidAlgebra.single_mul_single, DirectSum.of_mul_of]
