eval₂_mul_noncomm — Mathlib

English

Another form of evaluating finsupp polynomials via liftNC and powersHom.

Русский

Другой формат оценки полиномов, заданных finsupp, через liftNC и powersHom.

LaTeX

$$$\operatorname{ev}_{f,x}\{ toFinsupp := p \} = \operatorname{liftNC}(\uparrow f)(\text{powersHom } S\ x) p$$$

Lean4

theorem eval₂_mul_noncomm (hf : ∀ k, Commute (f <| q.coeff k) x) : eval₂ f x (p * q) = eval₂ f x p * eval₂ f x q :=
  by
  rcases p with ⟨p⟩; rcases q with ⟨q⟩
  simp only [coeff] at hf
  simp only [← ofFinsupp_mul, eval₂_ofFinsupp]
  exact liftNC_mul _ _ p q fun {k n} _hn => (hf k).pow_right n

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