Theorems · Theorem · order theory
abs_eq_abs
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a b : α}, |a| = |b| ↔ a = b ∨ a = -b- Cited by
- 7 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext
- Assumes
- AddGroupLinearOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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_negproof · cited by 960
- abs_negproof · cited by 93
- neg_eq_iff_eq_negproof · cited by 60
- abs_choiceproof · cited by 16
- eq_or_eq_neg_of_abs_eqproof · cited by 7
Cited by7
Results whose statement or proof uses this declaration.
- Polynomial.Chebyshev.eval_T_real_eq_neg_one_iffproof · cited by 3
- Polynomial.Chebyshev.eval_T_real_eq_one_iffproof · cited by 3
- NumberField.InfinitePlace.IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_ltproof · cited by 2
- Polynomial.isIntegral_of_mahlerMeasure_eq_oneproof · cited by 2
- Real.abs_cos_eq_one_iffproof · cited by 1
- NumberField.isUnit_iff_normproof · cited by 1
- Real.abs_sin_eq_one_iffproof · cited by 0