Commit 2026-09-09 05:30 feb73e2e

View on Github →

feat(Algebra/Regular/SMul): add IsSMulRegular.all (#43600) Generalise and rename isSMulRegular_of_group to IsSMulRegular.all. Requested by Eric in-person. The name is picked to match Commute.all.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Monic.lean

Modified Mathlib/Algebra/Polynomial/Roots.lean

Modified Mathlib/Algebra/Regular/SMul.lean

added theorem IsSMulRegular.all

modified theorem isSMulRegular_of_group