Theorems · Definition · commutative algebra
ValuativeRel.vle
{R : Type u_1} → {inst : Semiring R} → [self : ValuativeRel R] → R → R → PropThe valuation less-equal operator arising from ValuativeRel.
- Cited by
- 84 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- ValuativeRel
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
Cited by96
Results whose statement or proof uses this declaration.
- ValuativeRel.vltproof · cited by 49
- ValuativeRel.veqproof · cited by 27
- ValuativeRel.isEquivproof · cited by 6
- ValuativeRel.mul_vle_mul_leftstatement · cited by 6
- ValuativeRel.ValueGroupWithZero.liftstatement and proof · cited by 6
- ValuativeRel.mul_vle_mul_iff_leftstatement and proof · cited by 5
- ValuativeRel.mul_vle_mul_rightstatement and proof · cited by 5
- ValuativeRel.vle_reflstatement · cited by 4
- ValuativeRel.veq.vlestatement · cited by 4
- ValuativeRel.vle.transstatement · cited by 4
- ValuativeRel.vle.trans_vltstatement · cited by 4
- ValuativeRel.vlt.trans_vlestatement · cited by 4