mathlib3

7ccf4635 - feat(algebra): is_smul_regular for `pi`, `finsupp`, `matrix`, `polynomial` (#8716)

feat(algebra): is_smul_regular for `pi`, `finsupp`, `matrix`, `polynomial` (#8716) Also provide same lemma for finsupp, and specialize it for matrices and polynomials Inspired by https://github.com/leanprover-community/mathlib/pull/8681#discussion_r689320217 https://github.com/leanprover-community/mathlib/pull/8679#discussion_r689545373