Mathlib Map

Theorems · Theorem · order theory

mabs_le

∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G}, |a|ₘ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
Defined in
Mathlib.Algebra.Order.Group.Abs
Cited by
3 results in Mathlib
Foundations
Depth 28 from the axioms · uses propext, Quot.sound
Assumes
CommGroupLinearOrderIsOrderedMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

mabs_div_le_iff · cited by 4mabs_div_le_iffinv_le_of_mabs_le · cited by 0inv_le_of_mabs_lele_of_mabs_le · cited by 0le_of_mabs_leLinearOrder · cited by 8572LinearOrderCommGroup · cited by 990CommGroupIsOrderedMonoid · cited by 577IsOrderedMonoidmabs · cited by 148mabsinv_le' · cited by 5inv_le'mabs_le' · cited by 3mabs_le'mabs_leCITED BYCITES

Cites6

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

Cited by3

Results whose statement or proof uses this declaration.