Theorem Polynomial.primPart_ne_zero

Modification history

2026-01-20 16:34

Mathlib/RingTheory/Polynomial/Content.lean

chore(Algebra): deprecate `CancelMonoidWithZero` (#33851) …

Modified Polynomial.primPart_ne_zero View on Github →

2023-03-24 20:19

Mathlib/RingTheory/Polynomial/Content.lean

feat: port RingTheory.Polynomial.Content (#3066)

Added Polynomial.primPart_ne_zero View on Github →