Commit 2020-11-19 13:00 33265106
View on Github →chore(field_theory/minimal_polynomial): generalize irreducible (#5006)
I have removed the assumption that the base ring is a field for a minimal polynomial to be irreducible.
The proof is simple but long, it should be possible to use wlog to shorten it, but I do not understand how to do it...