PeriodicityLemma

📁 Source: Mathlib/Data/List/PeriodicityLemma.lean

Statistics

Metric	Count
Definitions HasPeriod	1
Theorems drop_of_hasPeriod_add, drop_prefix, factor, gcd, getElem?_mod, infix, take_append, hasPeriod_empty, hasPeriod_iff_forall_getElem?_mod, hasPeriod_iff_getElem?, hasPeriod_of_length_le, hasPeriod_zero	12
Total	13

List

Definitions

Name	Category	Theorems
HasPeriod 📖	MathDef	5 math math: hasPeriod_zero, hasPeriod_iff_forall_getElem?_mod, hasPeriod_of_length_le, hasPeriod_iff_getElem?, hasPeriod_empty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPeriod_empty 📖	mathematical	—	HasPeriod	—	Nat.instCanonicallyOrderedAdd
hasPeriod_iff_forall_getElem?_mod 📖	mathematical	—	HasPeriod	—	HasPeriod.getElem?_mod hasPeriod_iff_getElem?
hasPeriod_iff_getElem? 📖	mathematical	—	HasPeriod	—	HasPeriod.eq_1 min_eq_left_of_lt add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add Nat.instCanonicallyOrderedAdd add_comm
hasPeriod_of_length_le 📖	mathematical	—	HasPeriod	—	HasPeriod.eq_1 take_eq_self_iff
hasPeriod_zero 📖	mathematical	—	HasPeriod	—	—

List.HasPeriod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
drop_of_hasPeriod_add 📖	—	List.HasPeriod	—	—	List.hasPeriod_iff_getElem? add_comm
drop_prefix 📖	—	List.HasPeriod	—	—	—
factor 📖	—	List.HasPeriod	—	—	—
gcd 📖	—	List.HasPeriod	—	—	—
getElem?_mod 📖	—	List.HasPeriod	—	—	—
infix 📖	—	List.HasPeriod	—	—	factor
take_append 📖	—	List.HasPeriod	—	—	List.hasPeriod_iff_forall_getElem?_mod getElem?_mod inf_of_le_left le_of_not_gt

---

← Back to Index