Int.eq_zero_of_dvd_of_natAbs_lt_natAbs
theorem Int.eq_zero_of_dvd_of_natAbs_lt_natAbs : ∀ {a b : ℤ}, a ∣ b → b.natAbs < a.natAbs → b = 0
The theorem `Int.eq_zero_of_dvd_of_natAbs_lt_natAbs` states that for any two integers `a` and `b`, if `a` divides `b` and the absolute value of `b` is less than the absolute value of `a`, then `b` must be zero. Essentially, this theorem asserts that no integer can be divided by an integer with a larger absolute value without reducing to zero.
More concisely: If an integer `a` divides `b` and `|b| < |a|`, then `b` equals zero.
|
Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs
theorem Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs : ∀ {a b c : ℤ}, a % b = c → (a - c).natAbs < b.natAbs → a = c := by
sorry
This theorem states that for any three integers `a`, `b`, and `c`, if `a` modulo `b` equals `c`, and the absolute difference between `a` and `c` is less than the absolute value of `b`, then `a` equals `c`. Essentially, it expresses that if two integers are congruent with respect to a large enough modulus, they must be equal.
More concisely: If `a` is congruent to `c` modulo `b` and the absolute difference between `a` and `c` is less than the absolute value of `b`, then `a` equals `c`.
|