Theorems · Theorem · field theory

Polynomial.map_roots_comp_C_mul_X_add_C

∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R) (a b : R),
  IsUnit a → Multiset.map (fun x => a * x + b) (p.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)).roots = p.roots

Defined in

Mathlib.Algebra.Polynomial.Roots

Cited by

2 results in Mathlib

Foundations

Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomain