mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Feat(Algebra/Regular/SMul): Add some lemmas about `IsSMulRegular`

Open Shamrock-Frost opened this issue 1 year ago • 0 comments

Add some lemmas about IsSMulRegular.

I'm not sure if it's okay to add the Mathlib.GroupTheory.GroupAction.Hom import. My understanding is that this file is kept low in the hierarchy for some reason, but I'm not sure what that reason is or if this pushes it too far ahead. I added it for access to MulActionHomClass in isSMulRegular_of_injective_of_isSMulRegular.

Open in Gitpod

Shamrock-Frost avatar May 22 '24 20:05 Shamrock-Frost