Mathlib Map

Theorems · Theorem · order theory

Units.val_le_val

∀ {α : Type u_1} [inst : Monoid α] [inst_1 : Preorder α] {a b : αˣ}, ↑a ≤ ↑b ↔ a ≤ b
Defined in
Mathlib.Algebra.Order.Monoid.Units
Cited by
5 results in Mathlib
Foundations
Depth 13 from the axioms · uses propext
Assumes
MonoidPreorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered · cited by 4LinearOrderedCommGroupWit…Valuation.ltAddSubgroup_monotone · cited by 1Valuation.ltAddSubgroup_m…LaurentSeries.exists_Polynomial_intValuation_lt · cited by 1LaurentSeries.exists_Poly…Valuation.ltIdeal_mono · cited by 0Valuation.ltIdeal_monoValuativeRel.IsDiscrete.of_compatible_withZeroMulInt · cited by 0IsDiscrete.of_compatible_…Preorder · cited by 7952PreorderMonoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valUnits.val_le_valCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Preorderstatement and proof · cited by 7,952
  • Monoidstatement and proof · cited by 3,887
  • Unitsstatement and proof · cited by 2,804
  • Units.valstatement · cited by 1,966

Cited by5

Results whose statement or proof uses this declaration.