# Extensionality of monoid homs from `ℕ` #

source
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
source
theorem AddMonoidHom.ext_nat {A : Type u_2} [AddZeroClass A] {f g : ℕ →+ A} :
f 1 = g 1 → f = g
source
theorem AddMonoidHom.ext_nat_iff {A : Type u_2} [AddZeroClass A] {f g : ℕ →+ A} :
f = g ↔ f 1 = g 1
source
def multiplesHom (M : Type u_1) [AddMonoid M] :
M ≃ (ℕ →+ M)

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

Equations

- multiplesHom M = { toFun := fun (x : M) => { toFun := fun (n : ℕ) => n • x, map_zero' := ⋯, map_add' := ⋯ }, invFun := fun (f : ℕ →+ M) => f 1, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem multiplesHom_apply {M : Type u_1} [AddMonoid M] (x : M) (n : ℕ) :
((multiplesHom M) x) n = n • x
source
@[simp]
theorem multiplesHom_symm_apply {M : Type u_1} [AddMonoid M] (f : ℕ →+ M) :
(multiplesHom M).symm f = f 1
source
theorem AddMonoidHom.apply_nat {M : Type u_1} [AddMonoid M] (f : ℕ →+ M) (n : ℕ) :
f n = n • f 1
source
def powersHom (M : Type u_1) [Monoid M] :
M ≃ (Multiplicative ℕ →* M)

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

Equations

- powersHom M = Additive.ofMul.trans ((multiplesHom (Additive M)).trans AddMonoidHom.toMultiplicativeLeft)

Instances For

source
@[simp]
theorem powersHom_apply {M : Type u_1} [Monoid M] (x : M) (n : Multiplicative ℕ) :
((powersHom M) x) n = x ^ Multiplicative.toAdd n
source
@[simp]
theorem powersHom_symm_apply {M : Type u_1} [Monoid M] (f : Multiplicative ℕ →* M) :
(powersHom M).symm f = f (Multiplicative.ofAdd 1)
source
theorem MonoidHom.apply_mnat {M : Type u_1} [Monoid M] (f : Multiplicative ℕ →* M) (n : Multiplicative ℕ) :
f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n
source
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
source
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)
source
def multiplesAddHom (M : Type u_1) [AddCommMonoid M] :
M ≃+ (ℕ →+ M)

If `M` is commutative, `multiplesHom` is an additive equivalence.

Equations

- multiplesAddHom M = { toEquiv := multiplesHom M, map_add' := ⋯ }

Instances For

source
@[simp]
theorem multiplesAddHom_apply {M : Type u_1} [AddCommMonoid M] (x : M) (n : ℕ) :
((multiplesAddHom M) x) n = n • x
source
@[simp]
theorem multiplesAddHom_symm_apply {M : Type u_1} [AddCommMonoid M] (f : ℕ →+ M) :
(multiplesAddHom M).symm f = f 1
source
def powersMulHom (M : Type u_1) [CommMonoid M] :
M ≃* (Multiplicative ℕ →* M)

If `M` is commutative, `powersHom` is a multiplicative equivalence.

Equations

- powersMulHom M = { toEquiv := powersHom M, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem powersMulHom_apply {M : Type u_1} [CommMonoid M] (x : M) (n : Multiplicative ℕ) :
((powersMulHom M) x) n = x ^ Multiplicative.toAdd n
source
@[simp]
theorem powersMulHom_symm_apply {M : Type u_1} [CommMonoid M] (f : Multiplicative ℕ →* M) :
(powersMulHom M).symm f = f (Multiplicative.ofAdd 1)