Theorems · Theorem · order theory
AbsoluteValue.pos_iff
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
(abv : AbsoluteValue R S) {x : R}, 0 < abv x ↔ x ≠ 0- Cited by
- 6 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses no axioms
- Assumes
- SemiringSemiringPartialOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- PartialOrderstatement and proof · cited by 6,410
- AbsoluteValuestatement and proof · cited by 363
- LE.le.lt_iff_ne'proof · cited by 16
- AbsoluteValue.nonnegproof · cited by 16
- AbsoluteValue.ne_zero_iffproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- AbsoluteValue.posproof · cited by 12
- NumberField.InfinitePlace.pos_iffproof · cited by 6
- IsAbsoluteValue.abv_posproof · cited by 4
- AbsoluteValue.exists_one_lt_lt_one_of_not_isEquivproof · cited by 1
- AbsoluteValue.denseRange_algebraMap_piproof · cited by 1
- NumberField.FinitePlace.pos_iffproof · cited by 0