Commit 2023-02-14 09:08 b18ec142

View on Github →

feat: Port Data.Nat.Periodic (#2235)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Periodic.lean

added theorem Nat.Function.Periodic.map_mod_nat

added theorem Nat.filter_Ico_card_eq_of_periodic

added theorem Nat.filter_multiset_Ico_card_eq_of_periodic

added theorem Nat.periodic_coprime

added theorem Nat.periodic_gcd

added theorem Nat.periodic_mod