map_contract — Mathlib

English

Mapping commutes with contraction: for hp ≠ 0, map f (contract p q) = contract p (map f q).

Русский

Отображение сохраняет контракт: для hp ≠ 0, map f (contract p q) = contract p (map f q).

LaTeX

$$$\operatorname{map}(f)\bigl(\operatorname{contract}(p,q)\bigr) = \operatorname{contract}(p,\operatorname{map}(f,q))$$$

Lean4

theorem map_contract {p : ℕ} (hp : p ≠ 0) {f : R →+* S} {q : R[X]} : (q.contract p).map f = (q.map f).contract p :=
  ext fun n ↦ by simp only [coeff_map, coeff_contract hp]

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