Theorems · Theorem · number theory

Nat.count_modEq_card

∀ (b : ℕ) {r : ℕ}, 0 < r → ∀ (v : ℕ), Nat.count (fun x => x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0

There are b / r + [v % r < b % r] numbers in [0, b) congruent to v mod r, where [·] is the Iverson bracket.

Defined in

Mathlib.Data.Int.CardIntervalMod

Cited by

0 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound