Theorems · Theorem · field theory

Polynomial.mem_rootSet

∀ {T : Type w} [inst : CommRing T] {p : Polynomial T} {S : Type u_1} [IsDomain T] [inst_2 : CommRing S]
  [inst_3 : IsDomain S] [inst_4 : Algebra T S] [Module.IsTorsionFree T S] {a : S},
  a ∈ p.rootSet S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0

A version of mem_rootSet' that requires Module.IsTorsionFree and for the polynomial to be non-zero instead of requiring it to be non-zero after mapping.

Defined in

Mathlib.Algebra.Polynomial.Roots

Cited by

13 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingIsDomainAlgebraModule.IsTorsionFree