feat(algebra/*): Add of_injective lemmas (#5034)
This adds `free_monoid.of_injective`, `monoid_algebra.of_injective`, `add_monoid_algebra.of_injective`, and renames and restates `free_group.of.inj` to match these lemmas.
`function.injective (free_abelian_group.of)` is probably also true, but I wasn't able to prove it.
