Int.emod_two_eq_zero_or_one
theorem Int.emod_two_eq_zero_or_one : ∀ (n : ℤ), n % 2 = 0 ∨ n % 2 = 1
This theorem states that for every integer `n`, the remainder when `n` is divided by 2 is either 0 or 1. In other words, if you take any integer `n` and calculate `n modulo 2`, the result will always be either 0 (if `n` is even) or 1 (if `n` is odd).
More concisely: For every integer `n`, the remainder of `n` when divided by 2 is either 0 or 1. (Or equivalently, every integer `n` is congruent to 0 or 1 modulo 2.)
|
Int.exists_lt_and_lt_iff_not_dvd
theorem Int.exists_lt_and_lt_iff_not_dvd : ∀ (m : ℤ) {n : ℤ}, 0 < n → ((∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m)
This theorem establishes a relationship between non-divisibility and a number's position within a specific interval. Specifically, it states that for any integer `m` and a positive integer `n`, `m` is not divisible by `n` if and only if there exists another integer `k` such that `m` lies strictly between `n * k` and `n * (k + 1)`.
More concisely: For integers `m` and positive integer `n`, `m` is not divisible by `n` if and only if there exists an integer `k` such that `n * k < m < n * (k + 1)`.
|
Int.cast_mul_eq_zsmul_cast
theorem Int.cast_mul_eq_zsmul_cast : ∀ {α : Type u_1} [inst : AddCommGroupWithOne α] (m n : ℤ), ↑(m * n) = m • ↑n := by
sorry
This theorem states that for any additive commutative group with a multiplicative identity (denoted as `AddCommGroupWithOne α`), and for any integers `m` and `n`, the cast of the product of `m` and `n` equals to `m` multiplied by the cast of `n`. This operation is known as scalar multiplication (`•`). In other words, the theorem establishes that casting the product of two integers to this type is the same as performing scalar multiplication on the cast of one integer by the other. It's important to note that this theorem holds in a marginally broader context than the theorem `Int.cast_mul`.
More concisely: For any additive commutative group with a multiplicative identity `α` and for all integers `m` and `n`, `m * (CAST m.to_nat n) = CAST (m * n) to_add_monoid α`.
|