Commit 2020-04-29 07:43 f8fe5968
View on Github →chore(algebra/*): missing simp/inj lemmas (#2557)
Sometimes I have a specialized ext lemma for A →+ B that uses structure of A (e.g., A = monoid_algebra α R) and want to apply it to A →+* B or A →ₐ[R] B. These coe_*_inj lemmas make it easier.
Also add missing simp lemmas for bundled multiplication and rename pow_of_add and gpow_of_add to of_add_smul and of_add_gsmul, respectively.