chore({ring,group}_theory/free_*): Add of_injective (#5131)
This adds:
* `free_abelian_group.of_injective`
* `free_ring.of_injective`
* `free_comm_ring.of_injective`
* `free_algebra.of_injective`
following up from dcbec39a5bf9af5c6e065eea185f8776ac537d3b
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
