Commit 2021-04-12 05:36 193dd5bb

feat(algebra/{algebra, module}/basic): make 3 smultiplication by 1 simp lemmas (#7166) The three lemmas in the merged PR #7094 could be simp lemmas. This PR makes this suggestion. While I was at it,

• I moved one of the lemmas outside of the alg_hom namespace,
• I fixed a typo in a doc string of a tutorial. Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/trying.20out.20a.20.60simp.60.20lemma