Theorems · Theorem · order theory
one_le_mabs
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a : α), 1 ≤ |a|ₘ- Cited by
- 11 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- Latticestatement and proof · cited by 916
- MulLeftMonostatement and proof · cited by 410
- MulRightMonostatement and proof · cited by 263
- le_sup_rightproof · cited by 242
- sup_commproof · cited by 165
- pow_twoproof · cited by 150
- mabsstatement · cited by 148
- inv_mul_cancelproof · cited by 107
- sup_assocproof · cited by 37
- mul_supproof · cited by 6
- sup_mulproof · cited by 3
Cited by11
Results whose statement or proof uses this declaration.
- eq_of_mabs_div_le_oneproof · cited by 3
- sup_div_inf_eq_mabs_divproof · cited by 3
- oneLePart_mul_leOnePartproof · cited by 2
- mabs_mabsproof · cited by 2
- mabs_ne_oneproof · cited by 1
- mabs_sup_div_sup_le_mabsproof · cited by 1
- mabs_inf_div_inf_le_mabsproof · cited by 1
- MulArchimedeanClass.mk_le_mk_of_mabsproof · cited by 1
- leOnePart_mul_oneLePartproof · cited by 0
- MulArchimedeanClass.min_le_mk_of_le_of_leproof · cited by 0
- mabs_le_oneproof · cited by 0