Theorem Polynomial.integralNormalization_eval₂_leadingCoeff_mul_of_commute

Modification history

2024-12-02 07:36
Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
feat(Polynomial): new lemmas and noncommutative generalizations (#19665) …
Added Polynomial.integralNormalization_eval₂_leadingCoeff_mul_of_commuteView on Github →