mod_to_nat — Mathlib

English

For all n,d, the modulo operation on ZNum, when mapped to Nat, matches the corresponding Nat modulo after lifting through Num.

Русский

Для любых n,d модульная операция на ZNum, отображённая в Nat, совпадает с соответствующим остатком в Nat, полученным через Num.

LaTeX

$$$\forall n,d \in ZNum, ((n \% d : ZNum) : \mathbb{N}) = n % d$$$

Lean4

@[simp, norm_cast]
theorem mod_to_nat : ∀ n d, ((n % d : Num) : ℕ) = n % d
  | 0, 0 => by simp
  | 0, pos _ => (Nat.zero_mod _).symm
  | pos _, 0 => (Nat.mod_zero _).symm
  | pos _, pos _ => PosNum.mod'_to_nat _ _

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