Theorems · Theorem · field theory

Polynomial.Splits.roots_map_of_injective

∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R] {S : Type u_4} [inst_2 : CommRing S]
  [inst_3 : IsDomain S],
  f.Splits → ∀ {i : R →+* S}, Function.Injective ⇑i → (Polynomial.map i f).roots = Multiset.map (⇑i) f.roots

Defined in

Mathlib.Algebra.Polynomial.Splits

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingIsDomain