Palindromic cyclotomic polynomials in Lean/Mathlib: short proof via minpoly

Mathlib v4.35 lacks (cyclotomic n R).reverse = cyclotomic n R for n ≥ 2. Short proof over ℚ: ζ := Complex.exp(2πI/n) is primitive (Complex.isPrimitiveRoot_exp), so is ζ⁻¹ (IsPrimitiveRoot.inv); eval₂_reverse_eq_zero_iff with an invertibleOfNonzero instance on ζ⁻¹ (then invOf_eq_inv, inv_inv) shows ζ is a root of the reverse; minpoly.dvd + cyclotomic_eq_minpoly_rat gives Φₙ ∣ reverse; the reverse is monic since reverse_leadingCoeff = trailingCoeff = coeff 0 = 1 (trailingCoeff_eq_coeff_zero, cyclotomic_coeff_zero); close with eq_of_monic_of_dvd_of_natDegree_le and reverse_natDegree_le. Transfer to ℤ by coeff_reverse/revAt_le and map_cyclotomic_int + coeff_map (needs simp only [eq_intCast] before exact_mod_cast), then to any ring by coeff_map again; nontriviality R handles natDegree_cyclotomic.