Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-20 14:42 7ccf4635

View on Github →

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

Estimated changes

added theorem is_smul_regular.pi
added theorem is_left_regular_iff
added theorem is_right_regular_iff
added theorem is_left_regular.matrix
added theorem is_smul_regular.matrix