Rational square classes via p-adic valuations

Layer 1 of the Hasse–Minkowski development. A rational number q is a square in ℚ if and only if q is nonnegative and every one of its p-adic valuations is even.

The proof reduces q = q.num / q.den to the corresponding statement for naturals: an integer (resp. natural) is a square exactly when all exponents in its prime factorization are even. Since q.num and q.den are coprime, at most one of them is divisible by any given prime, so the evenness of the difference padicValRat p q = (q.num).factorization p - (q.den).factorization p forces the two exponents to be even individually.

Squares in ℕ

theorem HasseMinkowski.isSquare_nat_iff_even_factorization {n : ℕ} : IsSquare n ↔ ∀ (p : ℕ), Nat.Prime p → Even (n.factorization p)

theorem HasseMinkowski.factorization_eq_zero_or_eq_zero_of_coprime {a b p : ℕ} (hp : Nat.Prime p) (hab : a.Coprime b) : a.factorization p = 0 ∨ b.factorization p = 0

Rational squares via p-adic valuations

Since q.num and q.den are coprime, at most one of them is divisible by a given prime p, so only one of the two exponents in padicValRat p q is nonzero. Evenness of the difference therefore forces evenness of each exponent separately, which by isSquare_nat_iff_even_factorization makes both q.num and q.den squares.

theorem HasseMinkowski.padicValRat_eq_factorization {q : ℚ} {p : ℕ} (hp : Nat.Prime p) : padicValRat p q = ↑(q.num.natAbs.factorization p) - ↑(q.den.factorization p)

theorem HasseMinkowski.even_padicValRat_of_isSquare {q : ℚ} (hq : IsSquare q) (p : ℕ) (hp : Nat.Prime p) : Even (padicValRat p q)

theorem HasseMinkowski.nonneg_of_isSquare {q : ℚ} (hq : IsSquare q) : 0 ≤ q

theorem HasseMinkowski.Rat.isSquare_iff_even_padicValRat {q : ℚ} : IsSquare q ↔ 0 ≤ q ∧ ∀ (p : ℕ), Nat.Prime p → Even (padicValRat p q)

theorem HasseMinkowski.isSquare_of_nonneg_of_even_padicValRat {q : ℚ} (hq : 0 ≤ q) (h : ∀ (p : ℕ), Nat.Prime p → Even (padicValRat p q)) : IsSquare q