def AddChar.toAddMonoidHomAddChar {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommMonoid M] [Semiring R] [AddCommMonoid N] [Module R N] (γ : AddChar N M) : N →+ AddChar R M

Interpret a character of the R-module N as a homomorphism from N to character of R, via precomposition by scalar multiplication.

Equations

• γ.toAddMonoidHomAddChar = { toFun := fun (x : N) => { toFun := fun (r : R) => γ (r • x), map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddChar.toAddMonoidHomAddChar_apply_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommMonoid M] [Semiring R] [AddCommMonoid N] [Module R N] (γ : AddChar N M) (x : N) (r : R) : (γ.toAddMonoidHomAddChar x) r = γ (r • x)