Theorem Polynomial.natDegree_smul

Modification history

2026-01-20 08:34
Mathlib/Algebra/Polynomial/Degree/Domain.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality (#33873) …
Modified Polynomial.natDegree_smulView on Github →
2025-06-30 09:14
Mathlib/Algebra/Polynomial/Degree/Domain.lean
feat(Mathlib/Algebra/Polynomial/Degree/Domain.lean): generalize `natDegree_smul` from `SMulWithZero` to `SMulZeroClass` (#25257) …
Modified Polynomial.natDegree_smulView on Github →
2025-05-27 20:53
Mathlib/Algebra/Polynomial/Degree/Domain.lean
feat(Algebra/Polynomial/Degree/{Domain,Operations}): generalize some theorems to cover scalar multiplication with different types (#25237)
Modified Polynomial.natDegree_smulView on Github →
2024-12-09 08:03
Mathlib/Algebra/Polynomial/Degree/Domain.lean
feat(RingTheory/Polynomial/HilbertPoly): `Polynomial.natDegree_hilbertPoly_of_ne_zero` (#19765)
Added Polynomial.natDegree_smulView on Github →