Division_Alg
ProvedThe division algorithm for integers.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Division_Alg (a b : ℤ) (hb : b ≠ 0) : ∃ q r : ℤ, a = q * b + r ∧ 0 ≤ r ∧ r < |b| := by sorry
The division algorithm for integers.
import Mathlib.Analysis.Complex.Basic
theorem Division_Alg (a b : ℤ) (hb : b ≠ 0) : ∃ q r : ℤ, a = q * b + r ∧ 0 ≤ r ∧ r < |b| := by sorry