div'_to_nat — Mathlib

English

The division operator div' on PosNum, when interpreted as a natural number, agrees with ordinary natural-number division.

Русский

Оператор деления div' на PosNum, когда его рассматривать как натуральное число, согласуется с обычным делением в натуральных числах.

LaTeX

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

Lean4

@[simp]
theorem div'_to_nat (n d) : (div' n d : ℕ) = n / d :=
  (divMod_to_nat _ _).1.symm

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