aroots_map — Mathlib

English

Base-change along an algebra map preserves the multiset of roots: the roots of p after mapping coefficients agree with the roots of p.

Русский

Основание по алгебраическому отображению сохраняет мультисет корней: корни образа p совпадают с корнями p.

LaTeX

$$$$ (p.map(\mathrm{algebraMap}_{T \to S})).aroots_R = p.aroots_R $$$$

Lean4

@[simp]
theorem aroots_map (p : T[X]) [CommRing S] [Algebra T S] [Algebra S R] [Algebra T R] [IsScalarTower T S R] :
    (p.map (algebraMap T S)).aroots R = p.aroots R := by
  rw [aroots_def, aroots_def, map_map, IsScalarTower.algebraMap_eq T S R]

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