aeval_ite_mem_eq_self — Mathlib

English

If for all i in p.vars, g(i) = 0, then aeval g p equals algebraMap of the constant coefficient of p.

Русский

Если для всех i в p.vars выполняется g(i) = 0, то aeval g p равно отображению алгебры от константного коэффициента p.

LaTeX

$$$ aeval\ g\ p = algebraMap\ _\ _ (constantCoeff\ p) $$$

Lean4

theorem aeval_ite_mem_eq_self (q : MvPolynomial σ R) {s : Set σ} (hs : q.vars.toSet ⊆ s) [∀ i, Decidable (i ∈ s)] :
    MvPolynomial.aeval (fun i ↦ if i ∈ s then .X i else 0) q = q :=
  by
  rw [MvPolynomial.as_sum q, MvPolynomial.aeval_sum]
  refine Finset.sum_congr rfl fun u hu ↦ ?_
  rw [MvPolynomial.aeval_monomial, MvPolynomial.monomial_eq]
  congr 1
  exact Finsupp.prod_congr (fun i hi ↦ by simp [hs ((MvPolynomial.mem_vars _).mpr ⟨u, hu, hi⟩)])

Похожие утверждения