Theorem Polynomial.Splits.roots_map_of_injective

Modification history

2026-01-26 08:43
Mathlib/Algebra/Polynomial/Splits.lean
feat(Algebra/Polynomial/Splits): add `Splits.image_rootSet_of_monic` (#34046) …
Added Polynomial.Splits.roots_map_of_injectiveView on Github →