multSum_eq_main_err — Mathlib

English

For every d, the total weight of multiples of d equals the main term ν(d) times total mass plus the remainder.

Русский

Для каждого d сумма весов кратных d равна главному члену ν(d) умноженному на общую массу плюс остаток.

LaTeX

$$multSum(d) = nu(d) * totalMass + rem(d)$$

Lean4

theorem multSum_eq_main_err (d : ℕ) : s.multSum d = s.nu d * s.totalMass + s.rem d :=
  by
  dsimp [rem]
  ring

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