Commit 2024-11-13 23:44 739ad2d1
View on Github →chore: merge Algebra.Polynomial.Induction into RingTheory.Polynomial.Basic (#18996) This file no longer has anything to do with induction, and it seemed easier to drop these 3 lemmas into a file that already covers ideals of polynomials than to come up with a better place.