cast_sub — Mathlib

English

For any R with an additive group structure, and natural m ≤ n, the cast of (n − m) equals n − m in R.

Русский

Для любого кольца R с группой сложения и натуральные m ≤ n, отображение (n − m) в R равно n − m в R.

LaTeX

$$$((n - m) : R) = n - m \quad (m \le n)$$$

Lean4

@[simp, norm_cast]
theorem cast_sub {m n} (h : m ≤ n) : ((n - m : ℕ) : R) = n - m :=
  eq_sub_of_add_eq <| by rw [← cast_add, Nat.sub_add_cancel h]

Похожие утверждения