Extensionality of monoid homs from ℕ

theorem ext_nat' {A : Type u_2} {F : Type u_4} [FunLike F ℕ A] [AddZeroClass A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) : f = g

theorem AddMonoidHom.ext_nat {A : Type u_2} [AddZeroClass A] {f g : ℕ →+ A} : f 1 = g 1 → f = g

theorem AddMonoidHom.ext_nat_iff {A : Type u_2} [AddZeroClass A] {f g : ℕ →+ A} : f = g ↔ f 1 = g 1

def multiplesHom (M : Type u_1) [AddMonoid M] : M ≃ (ℕ →+ M)

Additive homomorphisms from ℕ are defined by the image of 1.

@[simp]

theorem multiplesHom_apply {M : Type u_1} [AddMonoid M] (x : M) (n : ℕ) : ((multiplesHom M) x) n = n • x

@[simp]

theorem multiplesHom_symm_apply {M : Type u_1} [AddMonoid M] (f : ℕ →+ M) : (multiplesHom M).symm f = f 1

theorem AddMonoidHom.apply_nat {M : Type u_1} [AddMonoid M] (f : ℕ →+ M) (n : ℕ) : f n = n • f 1

def powersHom (M : Type u_1) [Monoid M] : M ≃ (Multiplicative ℕ →* M)

Monoid homomorphisms from Multiplicative ℕ are defined by the image of Multiplicative.ofAdd 1.

@[simp]

theorem powersHom_apply {M : Type u_1} [Monoid M] (x : M) (n : Multiplicative ℕ) : ((powersHom M) x) n = x ^ Multiplicative.toAdd n

@[simp]

theorem powersHom_symm_apply {M : Type u_1} [Monoid M] (f : Multiplicative ℕ →* M) : (powersHom M).symm f = f (Multiplicative.ofAdd 1)

theorem MonoidHom.apply_mnat {M : Type u_1} [Monoid M] (f : Multiplicative ℕ →* M) (n : Multiplicative ℕ) : f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n

theorem MonoidHom.ext_mnat {M : Type u_1} [Monoid M] ⦃f g : Multiplicative ℕ →* M⦄ (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g

theorem MonoidHom.ext_mnat_iff {M : Type u_1} [Monoid M] {f g : Multiplicative ℕ →* M} : f = g ↔ f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)

def multiplesAddHom (M : Type u_1) [AddCommMonoid M] : M ≃+ (ℕ →+ M)

If M is commutative, multiplesHom is an additive equivalence.

@[simp]

theorem multiplesAddHom_apply {M : Type u_1} [AddCommMonoid M] (x : M) (n : ℕ) : ((multiplesAddHom M) x) n = n • x

@[simp]

theorem multiplesAddHom_symm_apply {M : Type u_1} [AddCommMonoid M] (f : ℕ →+ M) : (multiplesAddHom M).symm f = f 1

def powersMulHom (M : Type u_1) [CommMonoid M] : M ≃* (Multiplicative ℕ →* M)

If M is commutative, powersHom is a multiplicative equivalence.

@[simp]

theorem powersMulHom_apply {M : Type u_1} [CommMonoid M] (x : M) (n : Multiplicative ℕ) : ((powersMulHom M) x) n = x ^ Multiplicative.toAdd n

@[simp]

theorem powersMulHom_symm_apply {M : Type u_1} [CommMonoid M] (f : Multiplicative ℕ →* M) : (powersMulHom M).symm f = f (Multiplicative.ofAdd 1)