Legendre symbols and square-class changes of radicand

Replacing an integer a by a * u ^ 2, with p ∤ u, changes neither whether p divides it nor its Legendre symbol modulo p. This file records that elementary single-variable API: the positive divisibility equivalence dvd_mul_sq_iff and its negation not_dvd_mul_sq_iff, and the Legendre-symbol invariance legendreSym_mul_sq, together with indexed-family wrappers in the form used by the multiquadratic splitting law.

These facts are generic Legendre-symbol and divisibility statements.

@[simp]

theorem TauCeti.dvd_mul_sq_iff {p : ℕ} [Fact (Nat.Prime p)] {a u : ℤ} (hu : ¬↑p ∣ u) : ↑p ∣ a * u ^ 2 ↔ ↑p ∣ a

For u with p ∤ u, the prime p divides a * u ^ 2 exactly when it divides a.

theorem TauCeti.not_dvd_mul_sq_iff {p : ℕ} [Fact (Nat.Prime p)] {a u : ℤ} (hu : ¬↑p ∣ u) : ¬↑p ∣ a * u ^ 2 ↔ ¬↑p ∣ a

Multiplying by u ^ 2 with p ∤ u preserves non-divisibility by p.

@[simp]

theorem TauCeti.legendreSym_mul_sq {p : ℕ} [Fact (Nat.Prime p)] {a u : ℤ} (hu : ¬↑p ∣ u) : legendreSym p (a * u ^ 2) = legendreSym p a

Multiplying an integer by u ^ 2 with p ∤ u does not change its Legendre symbol.

theorem TauCeti.forall_legendreSym_eq_of_forall_eq_mul_sq {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {d e u : ι → ℤ} (he : ∀ (i : ι), e i = d i * u i ^ 2) (hu : ∀ (i : ι), ¬↑p ∣ u i) (i : ι) : legendreSym p (e i) = legendreSym p (d i)

Replacing each radicand in a family by d i * u i ^ 2 with p ∤ u i preserves all the Legendre symbols pointwise.

theorem TauCeti.forall_legendreSym_eq_one_iff_of_forall_eq_mul_sq {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {d e u : ι → ℤ} (he : ∀ (i : ι), e i = d i * u i ^ 2) (hu : ∀ (i : ι), ¬↑p ∣ u i) : (∀ (i : ι), legendreSym p (e i) = 1) ↔ ∀ (i : ι), legendreSym p (d i) = 1

The quadratic-residue conditions of a family are unchanged by replacing each radicand by d i * u i ^ 2 with p ∤ u i.

theorem TauCeti.forall_not_dvd_iff_of_forall_eq_mul_sq {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {d e u : ι → ℤ} (he : ∀ (i : ι), e i = d i * u i ^ 2) (hu : ∀ (i : ι), ¬↑p ∣ u i) : (∀ (i : ι), ¬↑p ∣ e i) ↔ ∀ (i : ι), ¬↑p ∣ d i

The unramifiedness conditions of a family are unchanged by replacing each radicand by d i * u i ^ 2 with p ∤ u i.