Parity of divisor counts

12 fully proved

Involutions and parity

TheoremSums invariant under a fixed-point-free involution are even#✓fully proved

Let \(s\) be a finite subset of a type \(\alpha\), let \(f : \alpha \to \alpha\) satisfy \(f(a) \in s\), \(f(f(a)) = a\) and \(f(a) \neq a\) for every \(a \in s\), and let \(g : \alpha \to \mathbb{Z}\) satisfy \(g(f(a)) = g(a)\) for every \(a \in s\). Then \(\sum_{a \in s} g(a) = 2k\) for some integer \(k\).

theorem exists_sum_eq_two_mul_of_involution {α : Type*} {s : Finset α} {f : α → α}
    {g : α → ℤ} (hmap : ∀ a ∈ s, f a ∈ s)
    (hinv : ∀ a ∈ s, f (f a) = a) (hfix : ∀ a ∈ s, f a ≠ a)
    (hg : ∀ a ∈ s, g (f a) = g a) :
    ∃ k : ℤ, ∑ a ∈ s, g a = 2 * k

Used by 2

Used byA fixed-point-free involution forces even cardinality · Character divisor sums modulo 4

TheoremA fixed-point-free involution forces even cardinality#✓fully proved

Let \(s\) be a finite subset of a type \(\alpha\) and let \(f : \alpha \to \alpha\) satisfy \(f(a) \in s\), \(f(f(a)) = a\) and \(f(a) \neq a\) for every \(a \in s\). Then \(s\) has an even number of elements.

theorem even_card_of_involution {α : Type*} {s : Finset α} {f : α → α}
    (hmap : ∀ a ∈ s, f a ∈ s) (hinv : ∀ a ∈ s, f (f a) = a)
    (hfix : ∀ a ∈ s, f a ≠ a) : Even s.card

Uses 1 · Used by 2

Proof usesSums invariant under a fixed-point-free involution are even

Used byA nonsquare has an even number of divisors · Squares are exactly the numbers with an odd number of divisors

TheoremHalf a sum of even numbers modulo 2#✓fully proved

Let \(s\) be a finite set of natural numbers and let \(f : \mathbb{N} \to \mathbb{N}\) be a function such that \(f(k)\) is even for every \(k \in s\). Then the natural number \(\frac{1}{2} \sum_{k \in s} f(k)\) is congruent modulo \(2\) to the number of elements \(k \in s\) with \(f(k) \equiv 2 \pmod 4\).

theorem sum_div_two_mod_two_eq_card_filter (s : Finset ℕ) (f : ℕ → ℕ)
    (heven : ∀ k ∈ s, Even (f k)) :
    ((∑ k ∈ s, f k) / 2) % 2
      = (Finset.filter (fun k => f k % 4 = 2) s).card % 2

Complementary divisors and divisor counts

TheoremComplementary divisor#✓fully proved

If \(n\) is a nonzero natural number and \(d\) is a divisor of \(n\), then \(n/d\) is also a divisor of \(n\).

theorem div_mem_divisors {n d : ℕ} (hd : d ∈ n.divisors) : n / d ∈ n.divisors

Used by 2

Used byA nonsquare has an even number of divisors · Character divisor sums modulo 4

TheoremThe complementary divisor of the complementary divisor#✓fully proved

If \(n\) is a nonzero natural number and \(d\) is a divisor of \(n\), then \(n/(n/d) = d\).

theorem div_div_self_of_mem_divisors {n d : ℕ} (hd : d ∈ n.divisors) : n / (n / d) = d

Used by 2

Used byA nonsquare has an even number of divisors · Character divisor sums modulo 4

TheoremComplementary divisors of a nonsquare are distinct#✓fully proved

If \(n\) is a natural number that is not a perfect square and \(d\) is a divisor of \(n\), then \(n/d \neq d\).

theorem div_ne_of_mem_divisors_of_not_isSquare {n d : ℕ} (hd : d ∈ n.divisors)
    (hsq : ¬ IsSquare n) : n / d ≠ d

Used by 2

Used byA nonsquare has an even number of divisors · Character divisor sums modulo 4

TheoremDivisor count of twice an odd number#✓fully proved

If \(u\) is an odd natural number, then \(2u\) has exactly twice as many positive divisors as \(u\).

theorem card_divisors_two_mul_of_odd {u : ℕ} (hu : Odd u) :
    (2 * u).divisors.card = 2 * u.divisors.card

TheoremA nonsquare has an even number of divisors#✓fully proved

If a natural number \(n\) is not a perfect square, then \(n\) has an even number of positive divisors.

theorem even_card_divisors_of_not_isSquare {n : ℕ} (hsq : ¬ IsSquare n) :
    Even n.divisors.card

Uses 4 · Used by 1

Proof usesA fixed-point-free involution forces even cardinality · The complementary divisor of the complementary divisor · Complementary divisor · Complementary divisors of a nonsquare are distinct

Used bySquares are exactly the numbers with an odd number of divisors

TheoremSquares are exactly the numbers with an odd number of divisors#✓fully proved

A nonzero natural number \(u\) has an odd number of positive divisors if and only if \(u\) is a perfect square.

theorem odd_card_divisors_iff_isSquare {u : ℕ} (hu : u ≠ 0) :
    Odd (Nat.divisors u).card ↔ IsSquare u

Uses 2

Proof usesA fixed-point-free involution forces even cardinality · A nonsquare has an even number of divisors

Quadratic characters

TheoremThe quadratic character mod 4 is ±1 on odd numbers#✓fully proved

Let \(\chi_4\) be the nontrivial character modulo \(4\) with values in \(\mathbb{Z}\): \(\chi_4(n) = 1\) for \(n \equiv 1 \pmod 4\), \(\chi_4(n) = -1\) for \(n \equiv 3 \pmod 4\), and \(\chi_4(n) = 0\) for even \(n\). For every odd natural number \(d\), \(\chi_4(d) = 1\) or \(\chi_4(d) = -1\).

theorem χ₄_nat_eq_one_or_neg_one_of_odd {d : ℕ} (hd : Odd d) :
    ZMod.χ₄ d = 1 ∨ ZMod.χ₄ d = -1

TheoremThe second quadratic character mod 8 is ±1 on odd numbers#✓fully proved

Let \(\chi_8'\) be the primitive quadratic character modulo \(8\) with values in \(\mathbb{Z}\) (the character of \(\mathbb{Q}(\sqrt{-2})\)): \(\chi_8'(n) = 1\) for \(n \equiv 1, 3 \pmod 8\), \(\chi_8'(n) = -1\) for \(n \equiv 5, 7 \pmod 8\), and \(\chi_8'(n) = 0\) for even \(n\). For every odd natural number \(d\), \(\chi_8'(d) = 1\) or \(\chi_8'(d) = -1\).

theorem χ₈'_nat_eq_one_or_neg_one_of_odd {d : ℕ} (hd : Odd d) :
    ZMod.χ₈' d = 1 ∨ ZMod.χ₈' d = -1

Multiplicative characters

TheoremCharacter divisor sums modulo 4#✓fully proved

Let \(N\) be a natural number and let \(\chi\) be a multiplicative character on \(\mathbb{Z}/N\mathbb{Z}\) with values in \(\mathbb{Z}\), applied to natural numbers through their residues modulo \(N\). Let \(n\) be a natural number that is not a perfect square such that \(\chi(n) = 1\) and \(\chi(d) \in \{1, -1\}\) for every positive divisor \(d\) of \(n\), and let \(\tau(n)\) be the number of positive divisors of \(n\). Then \(\sum_{d \mid n} \chi(d) \equiv \tau(n) \pmod 4\).

theorem sum_divisors_emod_four_eq_card {N : ℕ} (χ : MulChar (ZMod N) ℤ) {n : ℕ}
    (hpm : ∀ d ∈ n.divisors, χ d = 1 ∨ χ d = -1) (hn : χ n = 1) (hsq : ¬ IsSquare n) :
    (∑ d ∈ n.divisors, χ d) % 4 = (n.divisors.card : ℤ) % 4

Uses 4

Proof usesSums invariant under a fixed-point-free involution are even · The complementary divisor of the complementary divisor · Complementary divisor · Complementary divisors of a nonsquare are distinct

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.