Theorems · Theorem · order theory

Nat.cast_tsub

∀ {α : Type u_2} [inst : CommSemiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α]
  [inst_4 : Sub α] [OrderedSub α] [AddLeftReflectLE α] (m n : ℕ), ↑(m - n) = ↑m - ↑n

A version of Nat.cast_sub that works for ℝ≥0 and ℚ≥0. Note that this proof doesn't work for ℕ∞ and ℝ≥0∞, so we use type-specific lemmas for these types.

Defined in

Mathlib.Data.Nat.Cast.Order.Ring

Cited by

4 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringPartialOrderIsOrderedRingCanonicallyOrderedAddSubOrderedSubAddLeftReflectLE