Theorem Polynomial.IsWeaklyEisensteinAt.mul

Modification history

2025-06-03 12:11
Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean
feat(RingTheory/PowerSeries/WeierstrassPreparation): add algebra isomorphisms induced by Weierstrass division (#25087) …
Added Polynomial.IsWeaklyEisensteinAt.mulView on Github →