Squarefree elements, squares, and squarefree parts

This file records a few general facts about squarefree elements, squares, and rational squares that Mathlib does not provide directly, used across the multiquadratic development.

• Squarefree.not_isSquare: a squarefree non-unit of a monoid is not a square (the converse of Mathlib's IsUnit.squarefree). It is phrased with Squarefree dot-notation, so a caller holding ha : Squarefree a and hu : ¬ IsUnit a can write ha.not_isSquare hu.
• Squarefree.neg: negation preserves squarefreeness in any ring with distributive negation.
• not_isSquare_intCast_of_squarefree_of_ne_one: a squarefree integer other than 1 is not a rational square.
• isSquare_mul_sq_iff: in a commutative group with zero, multiplying by a nonzero square does not change squareness — the statement that squareness depends only on the square class.
• Int.exists_squarefree_mul_sq and Rat.exists_squarefree_int_mul_sq: the squarefree part. Every nonzero integer, and every nonzero rational, is a squarefree integer times a nonzero square. Mathlib's exists_sq_mul_squarefree proves the underlying factorization in a unique factorization monoid; the integer statement here records a nonzero square factor and puts the factors in the orientation used by the rational square-class argument.
• TauCeti.Int.not_four_dvd_of_squarefree and TauCeti.Int.emod_four_eq_two_or_three_of_squarefree: the modulo-four restrictions on squarefree integers.
• TauCeti.Int.emod_eight_eq_of_eq_mul_sq_of_not_four_dvd: removing a square factor preserves residues modulo eight when the original integer is not divisible by four.
• TauCeti.Int.emod_eight_eq_five_iff_exists_eq_mod_eight_eq_five_mul_sq and TauCeti.Int.exists_eq_mod_eight_eq_five_mul_sq_iff_exists_squarefree_mod_eight_eq_five_mul_sq: membership in the rational square class of an integer congruent to five modulo eight can be tested on an integer squarefree part.
• Nat.four_dvd_or_exists_odd_prime_and_dvd_of_squarefree: squarefreeness of every prime divisor of an n > 2, read in any ring, yields the single branch that Mathlib's Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt splits into. This is the bridge from a uniform hypothesis, which a caller can usually establish without knowing n, to the sharp branch-dependent one that a proof consumes.

theorem TauCeti.Int.not_four_dvd_of_squarefree {n : ℤ} (hn : Squarefree n) : ¬4 ∣ n

A squarefree integer is not divisible by four.

theorem TauCeti.Int.emod_four_eq_two_or_three_of_squarefree {n : ℤ} (hn : Squarefree n) (h : n % 4 ≠ 1) : n % 4 = 2 ∨ n % 4 = 3

A squarefree integer not congruent to one modulo four is congruent to two or three.

theorem Squarefree.not_isSquare {R : Type u_1} [Monoid R] {a : R} (ha : Squarefree a) (hu : ¬IsUnit a) : ¬IsSquare a

A squarefree non-unit of a monoid is not a square.

theorem Squarefree.neg {R : Type u_1} [Monoid R] [HasDistribNeg R] {n : R} (hn : Squarefree n) : Squarefree (-n)

Negation preserves squarefreeness in any monoid with distributive negation.

theorem not_isSquare_intCast_of_squarefree_of_ne_one {n : ℤ} (hsf : Squarefree n) (hne : n ≠ 1) : ¬IsSquare ↑n

A squarefree integer other than 1 is not a rational square.

theorem isSquare_mul_sq_iff {G₀ : Type u_1} [CommGroupWithZero G₀] {x y : G₀} (hy : y ≠ 0) : IsSquare (x * y ^ 2) ↔ IsSquare x

Squareness depends only on the square class. Multiplying by the square of a nonzero element does not change whether an element is a square.

theorem Int.exists_squarefree_mul_sq {n : ℤ} (hn : n ≠ 0) : ∃ (a : ℤ) (b : ℤ), Squarefree a ∧ b ≠ 0 ∧ n = a * b ^ 2

The squarefree part of an integer. Every nonzero integer is a squarefree integer times the square of a nonzero integer. This specializes Mathlib's unique-factorization-monoid theorem exists_sq_mul_squarefree to ℤ, makes the square factor's nonzeroness explicit, and reverses the factor order to the form used below.

theorem Rat.exists_squarefree_int_mul_sq {q : ℚ} (hq : q ≠ 0) : ∃ (a : ℤ) (c : ℚ), Squarefree a ∧ c ≠ 0 ∧ q = ↑a * c ^ 2

The squarefree part of a rational number. Every nonzero rational is a squarefree integer times the square of a nonzero rational: its square class is represented by a squarefree integer. This is what lets a square-class argument over ℚ work with squarefree integer radicands.

theorem TauCeti.Int.emod_eight_eq_of_eq_mul_sq_of_not_four_dvd {n s b : ℤ} (h : n = s * b ^ 2) (hn : ¬4 ∣ n) : n % 8 = s % 8

Removing an integer square factor preserves the residue modulo eight when the original integer is not divisible by four.

theorem TauCeti.Int.emod_eight_eq_five_iff_exists_eq_mod_eight_eq_five_mul_sq {n : ℤ} (hn : Squarefree n) : n % 8 = 5 ↔ ∃ (c : ℤ) (q : ℚ), c % 8 = 5 ∧ q ≠ 0 ∧ ↑n = ↑c * q ^ 2

For a squarefree integer, being in the rational square class of an integer congruent to five modulo eight is equivalent to being congruent to five modulo eight itself.

theorem TauCeti.Int.exists_eq_mod_eight_eq_five_mul_sq_iff_exists_squarefree_mod_eight_eq_five_mul_sq {n : ℤ} : (∃ (c : ℤ) (q : ℚ), c % 8 = 5 ∧ q ≠ 0 ∧ ↑n = ↑c * q ^ 2) ↔ ∃ (s : ℤ) (b : ℤ), Squarefree s ∧ b ≠ 0 ∧ n = s * b ^ 2 ∧ s % 8 = 5

An integer lies in the rational square class of an integer congruent to five modulo eight exactly when its squarefree part is congruent to five modulo eight. The nonzero integer square factor excludes zero, which has no squarefree part.

theorem Nat.four_dvd_or_exists_odd_prime_and_dvd_of_squarefree {R : Type u_1} [Ring R] {n : ℕ} (hn : 2 < n) (hsf : ∀ (p : ℕ), Prime p → p ∣ n → Squarefree ↑↑p) : 4 ∣ n ∧ Squarefree 2 ∨ ∃ (p : ℕ), Prime p ∧ p ≠ 2 ∧ p ∣ n ∧ Squarefree ↑↑p

From uniform squarefreeness to the sharp branch. If every prime dividing n > 2 is squarefree in R, then either 4 ∣ n and 2 is squarefree there, or some odd prime divides n and is squarefree there.

Mathlib's Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt supplies the dichotomy on n; what this adds is carrying the squarefreeness through it. The point of stating it is that the two hypotheses differ in usability: the uniform one can be established with no knowledge of n — over ℤ it is free, since every rational prime is squarefree — while the branch-dependent one is what a proof consumes. Anything proved from the sharp form is therefore available from the uniform form through this lemma.

The ambient ring may be noncommutative. Squarefree is a Monoid notion and the integer casts need AddGroupWithOne; Ring is the bundled class supplying both with a single 1, which is the unit IsUnit refers to inside Squarefree.