Theorem Polynomial.exists_monic_irreducible_factor

Modification history

2024-11-11 15:53
Mathlib/RingTheory/Polynomial/Basic.lean
chore: split UFD results out of RingTheory.Polynomial.Basic (#18875)
Modified Polynomial.exists_monic_irreducible_factorView on Github →
2024-02-15 16:16
Mathlib/RingTheory/Polynomial/Basic.lean
feat: add some simple results regarding polynomials (#10572) …
Added Polynomial.exists_monic_irreducible_factorView on Github →