Mathlib Map

Theorems · Theorem · order theory

toIcoMod_add_right

∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a (b + p) = toIcoMod hp a b
Defined in
Mathlib.Algebra.Order.ToIntervalMod
Cited by
2 results in Mathlib
Foundations
Depth 57 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.

toIcoMod_periodic · cited by 0toIcoMod_periodictoIcoMod_add_left · cited by 0toIcoMod_add_leftAddCommGroup · cited by 12871AddCommGroupLinearOrder · cited by 8572LinearOrderIsOrderedAddMonoid · cited by 1659IsOrderedAddMonoidArchimedean · cited by 603ArchimedeantoIcoMod · cited by 99toIcoModone_zsmul · cited by 59one_zsmultoIcoMod.congr_simp · cited by 25toIcoMod.congr_simptoIcoMod_add_zsmul · cited by 6toIcoMod_add_zsmultoIcoMod_add_rightCITED BYCITES

Cites8

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

Cited by2

Results whose statement or proof uses this declaration.