English
For any R with Ring structure and IsOrderedRing, the absolute value of the natural cast equals the cast: |(n : R)| = (n : R).
Русский
Для кольца R с упорядочиванием абсолютное значение натурального отображения равно самому отображению: |(n : R)| = (n : R).
LaTeX
$$|(n : R)| = (n : R)$$
Lean4
/-- 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. -/
@[simp, norm_cast]
theorem cast_tsub [CommSemiring α] [PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α]
[AddLeftReflectLE α] (m n : ℕ) : ↑(m - n) = (m - n : α) :=
by
rcases le_total m n with h | h
· rw [Nat.sub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]
exact mono_cast h
· rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩
rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]
