Commit 2025-06-30 09:14 4d039a4b
View on Github →feat(Mathlib/Algebra/Polynomial/Degree/Domain.lean): generalize natDegree_smul from SMulWithZero to SMulZeroClass (#25257)
as suggested by @eric-wieser in https://github.com/leanprover-community/mathlib4/pull/25237#discussion_r2111599865