Polynomial evaluation preserves coefficient agreement below a coordinate cutoff
ProvedMvPowerSeries.coeff_polynomial_algHom_eq_of_X_eq_belownumber-theoryopenai-pi-exponent-017
Two polynomial algebra homomorphisms into multivariate power series agree on all polynomial coefficients below a chosen coordinate cutoff whenever they agree there on every generator. The cutoff may be zero, in which case the conclusion's exponent hypothesis is impossible.
Preamble
import Mathlib.RingTheory.MvPowerSeries.Basic
Formal statement
theorem MvPowerSeries.coeff_polynomial_algHom_eq_of_X_eq_below
{σ τ R : Type*} [CommSemiring R]
(F G : MvPolynomial τ R →ₐ[R] MvPowerSeries σ R)
(j : σ) (T : ℕ)
(h : ∀ (i : τ) (b : σ →₀ ℕ), b j < T →
MvPowerSeries.coeff b (F (MvPolynomial.X i)) =
MvPowerSeries.coeff b (G (MvPolynomial.X i)))
(P : MvPolynomial τ R) (a : σ →₀ ℕ) (ha : a j < T) :
MvPowerSeries.coeff a (F P) = MvPowerSeries.coeff a (G P) := by sorrySource