English
If k is a CommSemiring and G a CommMonoid with compatible actions, then SkewMonoidAlgebra k G is a CommSemiring.
Русский
Если k — коммутативное полугруппа, G — коммутативный моноид с совместимыми действиями, то SkewMonoidAlgebra k G является коммутативным полугруппой-кольцом.
LaTeX
$$$ \text{CommSemiring}(SkewMonoidAlgebra k G) $$$
Lean4
instance instCommSemiring [CommSemiring k] [CommMonoid G] [MulSemiringAction G k] [SMulCommClass G k k] :
CommSemiring (SkewMonoidAlgebra k G) where
mul_comm a
b := by
have hgk (g : G) (r : k) : g • r = r := by rw [← Algebra.algebraMap_self_apply r, smul_algebraMap g r]
simp only [mul_def, hgk, sum_def]
rw [Finsupp.sum_comm]
exact Finsupp.sum_congr (fun x _ ↦ Finsupp.sum_congr (fun y _ ↦ by rw [mul_comm, mul_comm (a.toFinsupp y) _]))
