feat(algebra/*/basic): add trivial lemmas (#13416)
These save you from having to fiddle with `mul_one` when you want to rewrite them the other way, or allow easier commutativity rewrites.
Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
