Theorems · Theorem · order theory
Nat.cast_le
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
{m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n- Defined in
- Mathlib.Data.Nat.Cast.Order.Basic
- Cited by
- 159 results in Mathlib
- Foundations
- Depth 27 from the axioms, rests on 237 definitions · uses propext, Classical.choice, Quot.sound
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.
- PartialOrderstatement and proof · cited by 6,410
- CharZerostatement and proof · cited by 932
- AddLeftMonostatement and proof · cited by 687
- AddMonoidWithOnestatement and proof · cited by 313
- ZeroLEOneClassstatement and proof · cited by 304
- StrictMono.le_iff_leproof · cited by 104
- Nat.strictMono_castproof · cited by 12
Cited by159
Results whose statement or proof uses this declaration.
- Nat.one_le_castproof · cited by 21
- Nat.floor_natCastproof · cited by 19
- Set.ncard_le_ncardproof · cited by 15
- Polynomial.le_natDegree_of_ne_zeroproof · cited by 14
- SimpleGraph.chromaticNumber_le_iff_colorableproof · cited by 10
- Set.eq_of_subset_of_ncard_leproof · cited by 10
- Nat.cast_le_oneproof · cited by 6
- Nat.ceil_natCastproof · cited by 6
- Submodule.spanFinrank_span_le_ncard_of_finiteproof · cited by 5
- Set.ncard_image_leproof · cited by 5
- ONote.omega0_le_oaddproof · cited by 5
- Nat.cast_div_leproof · cited by 4