Commit 2024-02-13 23:17 1799b8c3

feat(Data/Polynomial): irreducibility of degree-{2,3} polynomials (#9697) The goal is to show that a degree 2 or 3 polynomial is irreducible iff it doesn't have roots. We already have Polynomial.Monic.irreducible_iff_natDegree' and some existing results in Lean 3: https://github.com/lean-forward/class-group-and-mordell-equation/blob/main/src/number_theory/assorted_lemmas.lean#L254 and the main work is to connect these bits together. I added a few helper lemmas about the "monicization" of a polynomial p, p * C (leadingCoeff p)⁻¹. Then I used these to show the Polynomial.Monic.irreducible_iff ... statements could be translated to (not necessarily monic) polynomials over a field, then I specialized these results to the degree-{2,3} case. I created a new file because I couldn't find an obvious place that imported both Polynomial.FieldDivision and Tactic.IntervalCases. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Polynomial.20irreducible