Residual coefficients of (X − 1)(X^r − 1)^N and (X^r − 1)^N /ₘ (X − 1)

Over any commutative ring, for r ≥ 3 and N ≥ 1:

• P = (X − 1)(X^r − 1)^N (degree L = N r + 1) has coeff P (L − 1) = −1 and coeff P (L − 2) = 0;
• Q = (X^r − 1)^N /ₘ (X − 1) (degree L = N r − 1, an exact quotient) has coeff Q (L − 1) = coeff Q (L − 2) = 1. Together with the identities NotaPuente.lemma_5_5 this gives τ₊ ∈ A when a1² − a2 is a unit of the subring A, and τ₋ ∈ A when a2 is.

The passage from "residue 1 modulo the radical" to "unit of the local order", and the identification of a1, a2 with the elementary symmetric functions of the roots of P or Q modulo the radical, are not formalized here.

Main results

• NotaPuente.Residues.coeff_P, NotaPuente.Residues.coeff_Q: the two top coefficients.
• NotaPuente.Residues.residue_P, NotaPuente.Residues.residue_Q: e1² − e2 = 1, resp. e2 = 1.
• NotaPuente.Residues.mem_of_mul_eq: d τ = n, n ∈ A, d a unit of A ⇒ τ ∈ A.
• NotaPuente.Residues.tau_plus_mem, NotaPuente.Residues.tau_minus_mem.

References

• C. Marín, Non-real orders of character values of GL(n), preprint (2026).
• C. Marín, The ring of character values depends only on the segment: SU(n), Sp(2m) and GL(n) at a torsion element, Zenodo (2026), doi:10.5281/zenodo.22847476.

theorem NotaPuente.Residues.coeff_pow_top {R : Type u_1} [CommRing R] {r : ℕ} (hr : 1 ≤ r) (N k : ℕ) : N * r < k + r → ((Polynomial.X ^ r - 1) ^ N).coeff k = if k = N * r then 1 else 0

Top coefficients of (X^r - 1)^N: for N r < k + r, the coefficient is 1 at k = N r, else 0 (i.e. (X^r - 1)^N = X^(N r) + (terms of degree ≤ N r - r)).

theorem NotaPuente.Residues.natDegree_pow_le' {R : Type u_1} [CommRing R] {r : ℕ} (hr : 1 ≤ r) (N : ℕ) : ((Polynomial.X ^ r - 1) ^ N).natDegree ≤ N * r

theorem NotaPuente.Residues.coeff_P {R : Type u_1} [CommRing R] {r N : ℕ} (hr : 3 ≤ r) (hN : 1 ≤ N) : ((Polynomial.X - 1) * (Polynomial.X ^ r - 1) ^ N).coeff (N * r + 1) = 1 ∧ ((Polynomial.X - 1) * (Polynomial.X ^ r - 1) ^ N).coeff (N * r) = -1 ∧ ((Polynomial.X - 1) * (Polynomial.X ^ r - 1) ^ N).coeff (N * r - 1) = 0

Lemma 5.6 (i), case L = N r + 1. For P = (X - 1)(X^r - 1)^N, r ≥ 3, N ≥ 1: coeff P L = 1, coeff P (L-1) = -1, coeff P (L-2) = 0, with L - 1 = N r, L - 2 = N r - 1. So e1 = -coeff P (L-1) = 1, e2 = coeff P (L-2) = 0.

theorem NotaPuente.Residues.mul_divByMonic_pow {R : Type u_1} [CommRing R] {r N : ℕ} (hN : 1 ≤ N) : (Polynomial.X - 1) * ((Polynomial.X ^ r - 1) ^ N /ₘ (Polynomial.X - 1)) = (Polynomial.X ^ r - 1) ^ N

(X - 1) * ((X^r - 1)^N /ₘ (X - 1)) = (X^r - 1)^N for N ≥ 1 (exact division).

theorem NotaPuente.Residues.coeff_Q {R : Type u_1} [CommRing R] {r N : ℕ} (hr : 3 ≤ r) (hN : 1 ≤ N) : ((Polynomial.X ^ r - 1) ^ N /ₘ (Polynomial.X - 1)).coeff (N * r - 1) = 1 ∧ ((Polynomial.X ^ r - 1) ^ N /ₘ (Polynomial.X - 1)).coeff (N * r - 2) = 1 ∧ ((Polynomial.X ^ r - 1) ^ N /ₘ (Polynomial.X - 1)).coeff (N * r - 3) = 1

Lemma 5.6 (i), case L = N r - 1. For Q = (X^r - 1)^N /ₘ (X - 1), r ≥ 3, N ≥ 1: coeff Q L = 1, coeff Q (L-1) = 1, coeff Q (L-2) = 1, with L = N r - 1. So e1 = -coeff Q (L-1) = -1, e2 = coeff Q (L-2) = 1.

theorem NotaPuente.Residues.residue_P {R : Type u_1} [CommRing R] {r N : ℕ} (hr : 3 ≤ r) (hN : 1 ≤ N) : (-((Polynomial.X - 1) * (Polynomial.X ^ r - 1) ^ N).coeff (N * r)) ^ 2 - ((Polynomial.X - 1) * (Polynomial.X ^ r - 1) ^ N).coeff (N * r - 1) = 1

Lemma 5.6 (ii), case L = N r + 1: e1² - e2 = 1, with e1 = -coeff P (L-1), e2 = coeff P (L-2).

theorem NotaPuente.Residues.residue_Q {R : Type u_1} [CommRing R] {r N : ℕ} (hr : 3 ≤ r) (hN : 1 ≤ N) : ((Polynomial.X ^ r - 1) ^ N /ₘ (Polynomial.X - 1)).coeff (N * r - 3) = 1 ∧ (-((Polynomial.X ^ r - 1) ^ N /ₘ (Polynomial.X - 1)).coeff (N * r - 2)) ^ 2 - ((Polynomial.X ^ r - 1) ^ N /ₘ (Polynomial.X - 1)).coeff (N * r - 3) = 0

Lemma 5.6 (ii), case L = N r - 1: e2 = coeff Q (L-2) = 1 (and e1² - e2 = 0).

Lemma 5.6 (iii): the algebraic step

theorem NotaPuente.Residues.mem_of_mul_eq {S : Type u_1} [CommRing S] (A : Subring S) {d e τ n : S} (he : e ∈ A) (hed : e * d = 1) (hn : n ∈ A) (h : d * τ = n) : τ ∈ A

If d τ = n with n ∈ A and d a unit of the subring A (e ∈ A, e d = 1), then τ ∈ A.

Lemma 5.5

a1, a2 and lemma_5_5 are those of Formalizations.RingTheory.Polynomial.CoefficientRing.StableIntervals (namespace NotaPuente).

theorem NotaPuente.Residues.tau_plus_mem {K : Type u_1} [Field K] (A : Subring K) {t : K} (ht : t ≠ 0) {L : ℕ} (hL : 2 ≤ L) (h1 : a1 t L ∈ A) (h2 : a2 t L ∈ A) {e : K} (he : e ∈ A) (hu : e * (a1 t L ^ 2 - a2 t L) = 1) : t ^ (↑L - 1) + t ^ (-(↑L - 1)) ∈ A

Lemma 5.6 (iii), τ₊. If a1, a2 ∈ A and a1² - a2 is a unit of A, then τ₊ = t^(L-1) + t^(-(L-1)) ∈ A.

theorem NotaPuente.Residues.tau_minus_mem {K : Type u_1} [Field K] (A : Subring K) {t : K} (ht : t ≠ 0) {L : ℕ} (hL : 2 ≤ L) (h1 : a1 t L ∈ A) (h2 : a2 t L ∈ A) {e : K} (he : e ∈ A) (hu : e * a2 t L = 1) : t ^ (↑L + 1) + t ^ (-(↑L + 1)) ∈ A

Lemma 5.6 (iii), τ₋. If a1, a2 ∈ A and a2 is a unit of A, then τ₋ = t^(L+1) + t^(-(L+1)) ∈ A.