Fundamental discriminants

A fundamental discriminant is an integer D ≡ 0, 1 mod 4 that is primitive, i.e. not a proper square multiple of a smaller discriminant. These are exactly the discriminants of quadratic fields.

The definition and the results below are elementary arithmetic on ℤ, so this file is kept independent of the theory of quadratic fields.

Main definitions

• Int.IsFundamentalDiscr: D is a fundamental discriminant.

Main results

• Int.isFundamentalDiscr_iff_squarefree: the concrete squarefree characterization, D ≡ 1 mod 4 squarefree or D = 4m with m squarefree and m ≡ 2, 3 mod 4.
• Int.isFundamentalDiscr_four_mul_add_one: 4m + 1 is a fundamental discriminant if and only if it is squarefree.
• Int.isFundamentalDiscr_four_mul: 4m is a fundamental discriminant if and only if m is squarefree and m ≡ 2, 3 mod 4.
• Int.isFundamentalDiscr_iff_forall_prime: the characterization uniform in the prime p, where the clause singling out p = 2 in the definition disappears.

def Int.IsFundamentalDiscr (D : ℤ) : Prop

D is a fundamental discriminant: it is a discriminant (D ≡ 0, 1 mod 4) and primitive, i.e. D / 4 ≢ 0, 1 mod 4 when 4 ∣ D, and no odd prime square divides D.

Equations

• D.IsFundamentalDiscr = ((D % 4 = 0 ∨ D % 4 = 1) ∧ (∀ (x : ℤ), D = 4 * x → ¬4 ∣ x ∧ x % 4 ≠ 1) ∧ ∀ (p : ℕ), Nat.Prime p → Odd p → ¬↑p ^ 2 ∣ D)

theorem Int.isFundamentalDiscr_def {D : ℤ} : D.IsFundamentalDiscr ↔ (D % 4 = 0 ∨ D % 4 = 1) ∧ (∀ (x : ℤ), D = 4 * x → ¬4 ∣ x ∧ x % 4 ≠ 1) ∧ ∀ (p : ℕ), Nat.Prime p → Odd p → ¬↑p ^ 2 ∣ D

theorem Int.IsFundamentalDiscr.ne_zero {D : ℤ} (h : D.IsFundamentalDiscr) : D ≠ 0

theorem Int.IsFundamentalDiscr.emod_four_eq_zero_or_one {D : ℤ} (h : D.IsFundamentalDiscr) : D % 4 = 0 ∨ D % 4 = 1

theorem Int.isFundamentalDiscr_iff_squarefree {D : ℤ} : D.IsFundamentalDiscr ↔ D % 4 = 1 ∧ Squarefree D ∨ D % 4 = 0 ∧ Squarefree (D / 4) ∧ (D / 4 % 4 = 2 ∨ D / 4 % 4 = 3)

D is a fundamental discriminant if and only if either D ≡ 1 mod 4 and D is squarefree, or D = 4 * d with d squarefree and d ≡ 2, 3 mod 4.

theorem Int.isFundamentalDiscr_iff_forall_prime {D : ℤ} : D.IsFundamentalDiscr ↔ (D % 4 = 0 ∨ D % 4 = 1) ∧ ∀ (p : ℕ), Nat.Prime p → ¬∃ (e : ℤ), D = ↑p ^ 2 * e ∧ (e % 4 = 0 ∨ e % 4 = 1)

Prime-by-prime characterisation of fundamental discriminants, uniform in p. Unlike the definition, which singles out p = 2, the second clause is the same for every prime.

theorem Int.isFundamentalDiscr_four_mul_add_one {m : ℤ} : (4 * m + 1).IsFundamentalDiscr ↔ Squarefree (4 * m + 1)

theorem Int.isFundamentalDiscr_four_mul {m : ℤ} : (4 * m).IsFundamentalDiscr ↔ Squarefree m ∧ (m % 4 = 2 ∨ m % 4 = 3)