cast_sub' — Mathlib

English

For m,n ∈ Num, (sub' m n : α) equals m − n in any α with AddGroupWithOne.

Русский

Для m,n ∈ Num, (sub' m n : α) равно m − n в любом α с AddGroupWithOne.

LaTeX

$$$$\forall \alpha\ [\text{AddGroupWithOne } \alpha],\ \forall m,n:\mathrm{Num},\ (\mathrm{sub}'\ m\ n : \alpha) = m - n.$$$$

Lean4

@[simp]
theorem cast_sub' [AddGroupWithOne α] : ∀ m n : Num, (sub' m n : α) = m - n
  | 0, 0 => (sub_zero _).symm
  | pos _a, 0 => (sub_zero _).symm
  | 0, pos _b => (zero_sub _).symm
  | pos _a, pos _b => PosNum.cast_sub' _ _

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