Lemmas about squares

Criteria for (non-)squareness in ℚ, ℤ and ZMod m.

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

theorem ZMod.isSquare_neg_one_of_isSquare_div {P Q : ℤ} {m : ℕ} (hQne : Q ≠ 0) (hPnegQ : ↑P = -↑Q) (hQunit : IsUnit ↑Q) (hsq : IsSquare (↑P / ↑Q)) : IsSquare (-1)

If P ≡ -Q mod m with Q a unit mod m and P/Q a rational square, then -1 is a square mod m.

theorem Nat.not_sq_add_sq_modEq_three (x y : ℕ) : ¬x ^ 2 + y ^ 2 ≡ 3 [MOD 4]

A sum of two squares is never congruent to 3 modulo 4, a square being 0 or 1.

theorem ZMod.not_isSquare_neg_one_of_dvd {m d : ℕ} (hdm : d ∣ m) (hd : d % 4 = 3) : ¬IsSquare (-1)

If d ∣ m with d ≡ 3 mod 4, then -1 is not a square in ZMod m.

theorem ZMod.not_isSquare_neg_one_of_four_dvd {m : ℕ} (hm : 4 ∣ m) : ¬IsSquare (-1)

If 4 ∣ m, then -1 is not a square in ZMod m.

theorem Int.isSquare_abs_of_isSquare_prod_of_pairwise_isCoprime {ι : Type u_1} (f : ι → ℤ) (S : Finset ι) (hcop : ∀ i ∈ S, ∀ j ∈ S, i ≠ j → IsCoprime (f i) (f j)) (hsq : IsSquare (∏ i ∈ S, f i)) (i : ι) : i ∈ S → IsSquare |f i|

If a family f is pairwise coprime on a finite set S and ∏_{i ∈ S} f i is a square, then |f i| is a square for every i ∈ S.

theorem prod_zpow_eq_zpow_sum {ι : Type u_1} {x : ℚ} (hx : x ≠ 0) (s : Finset ι) (e : ι → ℤ) : ∏ p ∈ s, x ^ e p = x ^ ∑ p ∈ s, e p

A product of fixed nonzero base and varying integer exponents collapses to a single power.