# mathlibdocumentation

data.nat.periodic

# Periodic Functions on ℕ #

This file identifies a few functions on ℕ which are periodic, and also proves a lemma about periodic predicates which helps determine their cardinality when filtering intervals over them.

theorem nat.periodic_gcd (a : ) :
theorem nat.periodic_coprime (a : ) :
theorem nat.periodic_mod (a : ) :
function.periodic (λ (n : ), n % a) a
theorem function.periodic.map_mod_nat {α : Type u_1} {f : → α} {a : } (hf : a) (n : ) :
f (n % a) = f n
theorem nat.filter_multiset_Ico_card_eq_of_periodic (n a : ) (p : → Prop) (pp : a) :
multiset.card (n + a))) = a

An interval of length a filtered over a periodic predicate of period a has cardinality equal to the number naturals below a for which p a is true.

theorem nat.filter_Ico_card_eq_of_periodic (n a : ) (p : → Prop) (pp : a) :
(n + a))).card = a

An interval of length a filtered over a periodic predicate of period a has cardinality equal to the number naturals below a for which p a is true.