Theorems · Definition · commutative algebra
ValuativeRel.vlt
{R : Type u_1} → [inst : Semiring R] → [ValuativeRel R] → R → R → PropThe valuation less-than relation, defined as x <ᵥ y ↔ ¬ y ≤ᵥ x.
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- SemiringValuativeRel
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- ValuativeRelstatement and proof · cited by 241
- ValuativeRel.vleproof · cited by 84
Cited by50
Results whose statement or proof uses this declaration.
- ValuativeRel.posSubmonoidproof · cited by 45
- ValuativeRel.mul_vle_mul_iff_leftstatement and proof · cited by 5
- ValuativeRel.vle.trans_vltstatement · cited by 4
- ValuativeRel.vlt.trans_vlestatement · cited by 4
- ValuativeRel.not_vlestatement · cited by 4
- ValuativeRel.mul_vlt_mul_leftstatement and proof · cited by 3
- ValuativeRel.not_vltstatement · cited by 3
- Valuation.vlt_iff_ltstatement and proof · cited by 2
- ValuativeRel.vle.not_vltstatement · cited by 2
- ValuativeRel.vlt.vlestatement and proof · cited by 2
- ValuativeRel.mul_vle_mul_iff_rightstatement and proof · cited by 2
- ValuativeRel.mul_vlt_mul_iff_leftstatement and proof · cited by 2