Theorems · Theorem · order theory
abs_eq
∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G},
0 ≤ b → (|a| = b ↔ a = b ∨ a = -b)- Defined in
- Mathlib.Algebra.Order.Group.Abs
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- LinearOrderstatement and proof · cited by 8,572
- absstatement · cited by 1,814
- IsOrderedAddMonoidstatement and proof · cited by 1,659
- abs_of_nonnegproof · cited by 279
- abs_negproof · cited by 93
- eq_or_eq_neg_of_abs_eqproof · cited by 7
Cited by9
Results whose statement or proof uses this declaration.
- abs_mulproof · cited by 98
- PhragmenLindelof.horizontal_stripproof · cited by 3
- Topology.RelCWComplex.cellFrontier_one_eqproof · cited by 2
- Real.Angle.abs_toReal_eq_pi_div_two_iffproof · cited by 2
- orthonormalBasis_one_dimproof · cited by 1
- Int.sq_eq_one_of_sq_lt_fourproof · cited by 1
- Finset.small_alternating_nsmul_of_small_triplingproof · cited by 0
- Subgroup.hasDetPlusMinusOne_iff_abs_detproof · cited by 0