contentIdeal_map_eq_map_contentIdeal

English

The content ideal commutes with ring homomorphisms: (p.map f).contentIdeal = p.contentIdeal.map f.

Русский

Контент-идеал коммутирует с гомоморфизмами колец: contentIdeal(p.map f) = contentIdeal(p) map f.

LaTeX

$$$ (p.map\ f).contentIdeal = p.contentIdeal.map\ f $$$

Lean4

theorem contentIdeal_map_eq_map_contentIdeal (f : R →+* S) : (p.map f).contentIdeal = p.contentIdeal.map f :=
  by
  suffices span ((map f p).coeffs ∪ {0}) = span (f '' p.coeffs ∪ {0}) by simpa [contentIdeal_def, map_span]
  congr 1
  ext s
  by_cases hs : s = 0
  · simp [hs]
  · aesop (add simp mem_coeffs_iff)

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