Even polynomials as polynomials in X² + c

An even polynomial (one fixed by X ↦ -X) over a domain of characteristic ≠ 2 is a polynomial in X² + c.

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 Polynomial.X_sq_add_C_comp_neg_X {R : Type u_1} [CommRing R] (c : R) : (X ^ 2 + C c).comp (-X) = X ^ 2 + C c

X² + c is fixed by X ↦ -X.

theorem Associated.comp_neg_X {R : Type u_1} [CommRing R] {p q : Polynomial R} (h : Associated p q) : Associated (p.comp (-Polynomial.X)) (q.comp (-Polynomial.X))

X ↦ -X preserves being associated.

theorem Polynomial.normalize_normalize_comp_neg_X {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid (Polynomial R)] (p : Polynomial R) : normalize ((normalize p).comp (-X)) = normalize (p.comp (-X))

Normalizing before reflecting does not change the normalized reflection.

theorem Polynomial.comp_neg_X_eq_or_eq_neg_of_associated {R : Type u_1} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p ≠ 0) (h : Associated (p.comp (-X)) p) : p.comp (-X) = p ∨ p.comp (-X) = -p

Over a domain, a polynomial whose reflection is merely associated to it is fixed by X ↦ -X up to a sign.

@[simp]

theorem Polynomial.expand_two_comp_neg_X {R : Type u_1} [CommRing R] (h : Polynomial R) : ((expand R 2) h).comp (-X) = (expand R 2) h

A polynomial in X² is fixed by X ↦ -X.

theorem Polynomial.eq_expand_two_contract_of_comp_neg_X {R : Type u_1} [CommRing R] [NoZeroDivisors R] [NeZero 2] {b : Polynomial R} (hb : b.comp (-X) = b) : b = (expand R 2) (contract 2 b)

Over a domain of characteristic ≠ 2, a polynomial fixed by X ↦ -X is a polynomial in X².

theorem Polynomial.even_eq_comp_X_sq_add_C {R : Type u_1} [CommRing R] [NoZeroDivisors R] [NeZero 2] (c : R) (b : Polynomial R) (hb : b.comp (-X) = b) : ∃ (e : Polynomial R), b = e.comp (X ^ 2 + C c)

An even polynomial over a domain of characteristic ≠ 2 is a polynomial in X² + c.