Commit 2025-09-28 10:18 618aa6a5
View on Github →refactor(Algebra/Polynomial/Splits): generalize Polynomial.splits_map_iff from Field to CommRing (#30043)
Polynomial.splits_map_iff currently assumes K →+* L →+* F with K a CommRing, L a Field, and F a Field. But L can be generalized to a CommRing. This also allows for a golf in RingTheory/Invariant/Basic.lean.