Theorems · Theorem · commutative algebra

Polynomial.sup_ker_aeval_le_ker_aeval_mul

∀ {R : Type u} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : M →ₗ[R] M}
  {p q : Polynomial R}, ((Polynomial.aeval f) p).ker ⊔ ((Polynomial.aeval f) q).ker ≤ ((Polynomial.aeval f) (p * q)).ker

Defined in

Mathlib.RingTheory.Polynomial.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule