Commit 2026-08-05 13:54 89e65db4

View on Github →

chore: deduplicate theorem Polynomial.not_isField (#42337) Deduplicate the theorem stating ¬IsField (Polynomial R) which is duplicated as Polynomial.not_isField and Ideal.polynomial_not_isField.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Div.lean

deleted theorem Polynomial.not_isField

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/KrullDimension/Polynomial.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

deleted theorem Ideal.polynomial_not_isField

added theorem Polynomial.not_isField