Transporting CharZero accross injective AddMonoidHoms #
This file exists in order to avoid adding extra imports to other files in this subdirectory.
theorem
CharZero.of_addMonoidHom
{M : Type u_1}
{N : Type u_2}
[AddCommMonoidWithOne M]
[AddCommMonoidWithOne N]
[CharZero M]
(e : M →+ N)
(he : e 1 = 1)
(he' : Function.Injective ⇑e)
:
CharZero N