cast_divNat — Mathlib

English

For a ∈ ℕ and b ∈ ℕ with b ≠ 0, the division of naturals corresponds to the division in α after casting: (divNat a b)° = (a/b)° in α.

Русский

Для a ∈ ℕ и b ∈ ℕ с b ≠ 0, частное деления натуралов совпадает с частным деления после приведения в α: (divNat a b)° = (a/b)°.

LaTeX

$$$ (\operatorname{divNat} a b)^{\uparrow} = (a / b)^{\uparrow} $$$

Lean4

@[simp]
theorem cast_divNat (a b : ℕ) : (divNat a b : α) = a / b :=
  by
  rw [← cast_natCast, ← cast_natCast b, ← cast_div]
  congr
  ext
  apply Rat.mkRat_eq_div

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