Mathlib Map

Theorems · Theorem · order theory

abs_sub_comm

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

Around this declaration

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

max_sub_min_eq_abs · cited by 10max_sub_min_eq_absAddCircle.norm_eq · cited by 6AddCircle.norm_eqabs_max_sub_max_le_max · cited by 5abs_max_sub_max_le_maxabs_min_sub_min_le_max · cited by 4abs_min_sub_min_le_maxabs_sub_round_eq_min · cited by 3abs_sub_round_eq_minPell.exists_of_not_isSquare · cited by 3Pell.exists_of_not_isSqua…Int.abs_sub_lt_one_of_floor_eq_floor · cited by 3Int.abs_sub_lt_one_of_flo…PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real · cited by 2PhragmenLindelof.right_ha…Real.log_five_near_10 · cited by 2Real.log_five_near_10IsCauSeq.of_abv_le · cited by 2IsCauSeq.of_abv_leabs_abs_sub_abs_le_abs_sub · cited by 2abs_abs_sub_abs_le_abs_subReal.log_three_near_10 · cited by 2Real.log_three_near_10Real.log_two_near_10 · cited by 2Real.log_two_near_10EuclideanGeometry.Sphere.mul_dist_eq_abs_power · cited by 2Sphere.mul_dist_eq_abs_po…SameRay.norm_sub · cited by 2SameRay.norm_subAddGroup · cited by 4410AddGroupabs · cited by 1814absLattice · cited by 916Latticeneg_sub · cited by 272neg_subabs_neg · cited by 93abs_negabs_sub_commCITED BYCITES

Cites5

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
  • absstatement and proof · cited by 1,814
  • Latticestatement and proof · cited by 916
  • neg_subproof · cited by 272
  • abs_negproof · cited by 93

Cited by40

Results whose statement or proof uses this declaration.