Extensionality of monoid homs from ℕ
#
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
@[simp]
@[simp]
Monoid homomorphisms from Multiplicative ℕ
are defined by the image
of Multiplicative.ofAdd 1
.
Equations
Instances For
@[simp]
If M
is commutative, multiplesHom
is an additive equivalence.
Equations
- multiplesAddHom M = { toEquiv := multiplesHom M, map_add' := ⋯ }
Instances For
@[simp]
@[simp]
If M
is commutative, powersHom
is a multiplicative equivalence.
Equations
- powersMulHom M = { toEquiv := powersHom M, map_mul' := ⋯ }
Instances For
@[simp]