English
The algebra MonoidAlgebra R M carries the structure of a NonUnitalSemiring; associativity and distributivity properties hold for multiplication with zero, even though there is no multiplicative identity.
Русский
Алгебра MonoidAlgebra R M имеет структуру NonUnitalSemiring; ассоциативность и распределительность выполняются по отношению к умножению и нулю, хотя единицы умножения нет.
LaTeX
$$$\operatorname{NonUnitalSemiring}(\operatorname{MonoidAlgebra} \; R \; M)$$$
Lean4
@[to_additive (dont_translate := R)]
instance nonUnitalSemiring : NonUnitalSemiring (MonoidAlgebra R M) where
mul_assoc f g
h := by
-- Porting note: `reducible` cannot be `local` so proof gets long.
simp only [mul_def]
rw [sum_sum_index] <;> congr; on_goal 1 => ext a₁ b₁
rw [sum_sum_index, sum_sum_index] <;> congr; on_goal 1 => ext a₂ b₂
rw [sum_sum_index, sum_single_index] <;> congr; on_goal 1 => ext a₃ b₃
on_goal 1 => rw [sum_single_index, mul_assoc, mul_assoc]
all_goals
simp only [single_zero, single_add, forall_true_iff, add_mul, mul_add, zero_mul, mul_zero, sum_zero, sum_add]
