Mathlib Map

Theorems · Theorem · order theory

abs_neg

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

Around this declaration

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

abs_sub_comm · cited by 40abs_sub_commReal.log_neg_eq_log · cited by 27Real.log_neg_eq_logArchimedeanClass.mk_neg · cited by 15ArchimedeanClass.mk_negabs_eq · cited by 9abs_eqabs_eq_abs · cited by 7abs_eq_abssummable_pow_mul_jacobiTheta₂_term_bound · cited by 6summable_pow_mul_jacobiTh…Affine.Simplex.ExcenterExists.dist_excenter · cited by 6ExcenterExists.dist_excen…Polynomial.mahlerMeasure_mul · cited by 5Polynomial.mahlerMeasure_…Real.abs_log_sub_add_sum_range_le · cited by 4Real.abs_log_sub_add_sum_…HurwitzZeta.hasSum_nat_cosZeta · cited by 4HurwitzZeta.hasSum_nat_co…abs_sub · cited by 4abs_subPolynomial.Chebyshev.eval_T_real_eq_neg_one_iff · cited by 3Chebyshev.eval_T_real_eq_…Orientation.volumeForm_robust' · cited by 3Orientation.volumeForm_ro…Complex.abs_im_lt_norm · cited by 3Complex.abs_im_lt_normReal.summable_abs_int_rpow · cited by 3Real.summable_abs_int_rpowAddGroup · cited by 4410AddGroupabs · cited by 1814absneg_neg · cited by 960neg_negLattice · cited by 916Latticesup_comm · cited by 165sup_commabs_negCITED 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 · cited by 1,814
  • neg_negproof · cited by 960
  • Latticestatement and proof · cited by 916
  • sup_commproof · cited by 165

Cited by93

Results whose statement or proof uses this declaration.