mathlib

193dd5bb - feat(algebra/{algebra, module}/basic): make 3 smultiplication by 1 `simp` lemmas (#7166)

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