Periodic

📁 Source: Mathlib/Data/Nat/Periodic.lean

Statistics

Metric	Count
Definitions	0
Theorems map_mod_nat, filter_Ico_card_eq_of_periodic, filter_multiset_Ico_card_eq_of_periodic, periodic_coprime, periodic_gcd, periodic_mod	6
Total	6

Function.Periodic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mod_nat 📖	—	Function.Periodic	—	—	mul_comm Nat.nsmul_eq_mul nsmul

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
filter_Ico_card_eq_of_periodic 📖	mathematical	Function.Periodic	Finset.card Finset.filter Finset.Ico instPreorder instLocallyFiniteOrder count	—	filter_multiset_Ico_card_eq_of_periodic
filter_multiset_Ico_card_eq_of_periodic 📖	mathematical	Function.Periodic	Multiset.card Multiset.filter Multiset.Ico instPreorder instLocallyFiniteOrder count	—	count_eq_card_filter_range Finset.card.eq_1 Finset.filter_val Finset.range_val multiset_Ico_map_mod Multiset.map_count_True_eq_filter_card Multiset.map_map Function.Periodic.map_mod_nat
periodic_coprime 📖	mathematical	—	Function.Periodic	—	coprime_add_self_right
periodic_gcd 📖	mathematical	—	Function.Periodic	—	—
periodic_mod 📖	mathematical	—	Function.Periodic	—	—

---

← Back to Index