Commit 2026-08-17 20:58 818f61df
View on Github →chore(RingTheory/MvPolynomial/MonomialOrder): rename degree_subsingleton to degree_of_subsingleton (#42853)
In https://github.com/leanprover-community/mathlib4/pull/39736#discussion_r3786425002, a reviewer suggested a similar rename for a lemma that was being added, so this PR renames degree_subsingleton for consistency.