Theorem Polynomial.mem_nonZeroDivisors_of_leadingCoeff

Modification history

2025-04-07 16:44

Mathlib/Algebra/Polynomial/RingDivision.lean

feat(RingTheory): `dim R + 1 ≤ dim R[X]` (#21088) …

Modified Polynomial.mem_nonZeroDivisors_of_leadingCoeff View on Github →

2023-12-13 19:05

Mathlib/Data/Polynomial/RingDivision.lean

feat(Data/Polynomial/RingDivision): improvements to `Polynomial.rootMultiplicity` (#8563) …

Added Polynomial.mem_nonZeroDivisors_of_leadingCoeff View on Github →