Mathlib Map

Theorems · Theorem · order theory

toIcoMod_periodic

∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), Function.Periodic (toIcoMod hp a) p
Defined in
Mathlib.Algebra.Order.ToIntervalMod
Cited by
0 results in Mathlib
Foundations
Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommGroupLinearOrderIsOrderedAddMonoidArchimedean
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

QuotientAddGroup.equivIcoMod · cited by 5QuotientAddGroup.equivIco…AddCommGroup · cited by 12871AddCommGroupLinearOrder · cited by 8572LinearOrderIsOrderedAddMonoid · cited by 1659IsOrderedAddMonoidArchimedean · cited by 603ArchimedeanFunction.Periodic · cited by 154Function.PeriodictoIcoMod · cited by 99toIcoModtoIcoMod_add_right · cited by 2toIcoMod_add_righttoIcoMod_periodicCITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.