Mathlib Map

Theorems · Theorem · order theory

le_neg_self_iff

∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a : α}, a ≤ -a ↔ a ≤ 0
Defined in
Mathlib.Algebra.Order.Group.Defs
Cited by
1 results in Mathlib
Foundations
Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommGroupLinearOrderIsOrderedAddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

abs_eq_neg_self · cited by 14abs_eq_neg_selfAddCommGroup · cited by 12871AddCommGroupLinearOrder · cited by 8572LinearOrderIsOrderedAddMonoid · cited by 1659IsOrderedAddMonoidnot_le · cited by 328not_leneg_lt_self_iff · cited by 2neg_lt_self_iffle_neg_self_iffCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.