Theorem Polynomial.integralNormalization_degree

Modification history

2025-11-24 14:11

Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

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

Deleted Polynomial.integralNormalization_degree View on Github →

2024-11-30 18:25

Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

chore: remove `normalizeScaleRoots` (#6183) …

Added Polynomial.integralNormalization_degree View on Github →