Commit 2025-11-24 14:11 69a309a8

View on Github →

chore(RingTheory/Polynomial): deprecate integralNormalization_degree (#32049)

Estimated changes

Modified Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

deleted theorem Polynomial.integralNormalization_degree