Theorems · Theorem · order theory
abs_of_neg
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], a < 0 → |a| = -a- Cited by
- 39 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext
- Assumes
- LatticeAddGroupAddLeftMono
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- LT.lt.leproof · cited by 2,189
- absstatement · cited by 1,814
- Latticestatement and proof · cited by 916
- AddLeftMonostatement and proof · cited by 687
- abs_of_nonposproof · cited by 53
Cited by39
Results whose statement or proof uses this declaration.
- abs_posproof · cited by 45
- Real.rpow_def_of_negproof · cited by 7
- Real.abs_rpow_le_abs_rpowproof · cited by 7
- Complex.cos_argproof · cited by 7
- Orientation.oangle_add_right_smul_rotation_pi_div_twoproof · cited by 4
- hasStrictDerivAt_abs_negproof · cited by 3
- IsCoprime.abs_left_iffproof · cited by 3
- self_mul_signproof · cited by 3
- summable_abs_iffproof · cited by 3
- intervalIntegral.integral_comp_mul_rightproof · cited by 3
- Real.circleAverage_abs_radiusproof · cited by 2
- Hyperreal.infiniteNeg_iffproof · cited by 2