Mathlib Map

Theorems · Theorem · order theory

toIcoMod_sub_self

∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a b - b = -toIcoDiv hp a b • p
Defined in
Mathlib.Algebra.Order.ToIntervalMod
Cited by
2 results in Mathlib
Foundations
Depth 55 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_sub_self_eq_mul · cited by 0toIcoMod_sub_self_eq_mulReal.Angle.coe_toIcoMod · cited by 0Angle.coe_toIcoModAddCommGroup · cited by 12871AddCommGroupLinearOrder · cited by 8572LinearOrderIsOrderedAddMonoid · cited by 1659IsOrderedAddMonoidArchimedean · cited by 603Archimedeanneg_smul · cited by 306neg_smultoIcoMod · cited by 99toIcoModtoIcoDiv · cited by 84toIcoDivsub_sub_cancel_left · cited by 28sub_sub_cancel_lefttoIcoMod_sub_selfCITED 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.