Commit 2020-11-18 23:23 dcbec39a

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.