rw [mul_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
⊢ (zeta 𝕜 * zeta 𝕜) a b = ↑(Icc a b).card
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, 1