Squares modulo powers of two
Squares of natural numbers
TheoremSquares of natural numbers modulo 8#✓fully proved
For every natural number \(r\), the remainder of \(r^2\) on division by \(8\) is \(0\), \(1\) or \(4\).
theorem sq_mod_eight (r : ℕ) :
r ^ 2 % 8 = 0 ∨ r ^ 2 % 8 = 1 ∨ r ^ 2 % 8 = 4TheoremNumbers congruent to 3 mod 8 are not squares#✓fully proved
If a natural number \(n\) satisfies \(n \equiv 3 \pmod 8\), then \(n\) is not the square of a natural number.
theorem not_isSquare_of_mod_eight_eq_three {n : ℕ} (h : n % 8 = 3) : ¬ IsSquare nUses 1
TheoremNumbers congruent to 6 mod 8 are not squares#✓fully proved
If a natural number \(n\) satisfies \(n \equiv 6 \pmod 8\), then \(n\) is not the square of a natural number.
theorem not_isSquare_of_mod_eight_eq_six {n : ℕ} (h : n % 8 = 6) : ¬ IsSquare nUses 1
TheoremA number that is 6 mod 8 minus a smaller square is not a square#✓fully proved
Let \(N\) and \(k\) be natural numbers with \(N \equiv 6 \pmod 8\) and \(k^2 < N\). Then \(N - k^2\) is not the square of a natural number.
theorem not_isSquare_sub_sq_of_mod_eight_eq_six {N k : ℕ} (hN : N % 8 = 6)
(hk : k ^ 2 < N) : ¬ IsSquare (N - k ^ 2)Uses 1
TheoremOdd squares modulo 16#✓fully proved
For every odd natural number \(k\), either \(k^2 \equiv 1 \pmod{16}\) and \(k \equiv 1\) or \(7 \pmod 8\), or \(k^2 \equiv 9 \pmod{16}\) and \(k \equiv 3\) or \(5 \pmod 8\).
theorem sq_mod_sixteen_of_odd (k : ℕ) (hk : Odd k) :
(k ^ 2 % 16 = 1 ∧ (k % 8 = 1 ∨ k % 8 = 7)) ∨
(k ^ 2 % 16 = 9 ∧ (k % 8 = 3 ∨ k % 8 = 5))Squares of integers
TheoremSquares of integers modulo 8#✓fully proved
For every integer \(x\), the remainder of \(x^2\) on division by \(8\), taken in \(\{0, 1, \dots, 7\}\), is \(0\), \(1\) or \(4\).
theorem sq_emod_eight (x : ℤ) :
x ^ 2 % 8 = 0 ∨ x ^ 2 % 8 = 1 ∨ x ^ 2 % 8 = 4Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.