Theorems · Theorem · order theory
eq_or_eq_neg_of_abs_eq
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a b : α}, |a| = b → a = b ∨ a = -b- Cited by
- 7 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext
- Assumes
- AddGroupLinearOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement and proof · cited by 8,572
- AddGroupstatement and proof · cited by 4,410
- absstatement and proof · cited by 1,814
- neg_eq_iff_eq_negproof · cited by 60
- abs_choiceproof · cited by 16
Cited by7
Results whose statement or proof uses this declaration.
- abs_eqproof · cited by 9
- abs_eq_absproof · cited by 7
- Finset.small_nsmul_of_small_triplingproof · cited by 1
- Finset.small_pow_of_small_triplingproof · cited by 1
- LinearOrderedRing.orderOf_le_twoproof · cited by 0