Theorems · Theorem · order theory
abs_zero
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α], |0| = 0- Cited by
- 88 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
- absstatement · cited by 1,814
- le_rflproof · cited by 1,558
- Latticestatement and proof · cited by 916
- AddLeftMonostatement and proof · cited by 687
- abs_of_nonnegproof · cited by 279
Cited by88
Results whose statement or proof uses this declaration.
- abs_posproof · cited by 45
- Real.log_absproof · cited by 17
- MeasureTheory.Measure.addHaar_smulproof · cited by 13
- ArchimedeanClass.mk_eq_top_iffproof · cited by 7
- MeasureTheory.Measure.addHaar_image_linearMapproof · cited by 4
- ENNReal.abs_toRealproof · cited by 4
- HurwitzZeta.hasSum_nat_cosZetaproof · cited by 4
- Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zeroproof · cited by 3
- MeasureTheory.Measure.integral_comp_smulproof · cited by 3
- self_mul_signproof · cited by 3
- NumberField.Units.regOfFamily_eq_det'proof · cited by 3
- Finset.abs_sum_le_sum_absproof · cited by 3