Theorems · Theorem · commutative algebra

Polynomial.roots_scaleRoots

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R) {r : R},
  IsUnit r → (p.scaleRoots r).roots = Multiset.map (fun x => r * x) p.roots

Defined in

Mathlib.RingTheory.Polynomial.ScaleRoots

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain