mod'_to_nat

Mathlib.Data.Num.ZNum

URI: https://scilib.ai/kg/mathlib#PosNum.mod'_to_nat

English

The remainder function mod' on PosNum, when mapped to Nat, equals the standard remainder n mod d.

Русский

Остаток mod' на PosNum, отображённый в Нат, равен обычному остатку n mod d.

LaTeX

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

Lean4

@[simp]
theorem mod'_to_nat (n d) : (mod' n d : ℕ) = n % d :=
  (divMod_to_nat _ _).2.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru