multSum — Mathlib

English

The weight of all elements that are multiples of d is the sum over the support of the indicator d | n times the weight of n.

Русский

Вес суммирования элементов, кратных d, равен сумме по поддержке формулы: если d делит n, то вес n, иначе 0.

LaTeX

$$@[simp] multSum(d) = ∑_{n ∈ s.support} if d ∣ n then s.weights(n) else 0$$

Lean4

/-- The weight of all the elements that are a multiple of `d`. -/
@[simp]
def multSum (d : ℕ) : ℝ :=
  ∑ n ∈ s.support, if d ∣ n then s.weights n else 0

Похожие утверждения