Mathlib Map

Theorems · Theorem · order theory

abs_eq_max_neg

∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a : α}, |a| = max a (-a)
Defined in
Mathlib.Algebra.Order.Group.Unbundled.Abs
Cited by
2 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext
Assumes
AddGroupLinearOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

abs_eq_self · cited by 59abs_eq_selfabs_eq_neg_self · cited by 14abs_eq_neg_selfLinearOrder · cited by 8572LinearOrderAddGroup · cited by 4410AddGroupabs · cited by 1814absabs_eq_max_negCITED BYCITES

Cites3

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 · cited by 1,814

Cited by2

Results whose statement or proof uses this declaration.