Power as a monoid hom

theorem nsmulAddMonoidHom.proof_1 {α : Type u_1} [AddCommMonoid α] (n : ℕ) : n • 0 = 0

def nsmulAddMonoidHom {α : Type u_1} [AddCommMonoid α] (n : ℕ) : α →+ α

Multiplication by a natural n on a commutative additive monoid, considered as a morphism of additive monoids.

Equations

• nsmulAddMonoidHom n = { toZeroHom := { toFun := fun (x : α) => n • x, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem powMonoidHom_apply {α : Type u_1} [CommMonoid α] (n : ℕ) : ∀ (x : α), (powMonoidHom n) x = x ^ n

@[simp]

theorem nsmulAddMonoidHom_apply {α : Type u_1} [AddCommMonoid α] (n : ℕ) : ∀ (x : α), (nsmulAddMonoidHom n) x = n • x

def powMonoidHom {α : Type u_1} [CommMonoid α] (n : ℕ) : α →* α

The nth power map on a commutative monoid for a natural n, considered as a morphism of monoids.

Equations

• powMonoidHom n = { toOneHom := { toFun := fun (x : α) => x ^ n, map_one' := ⋯ }, map_mul' := ⋯ }

def zsmulAddGroupHom {α : Type u_1} [SubtractionCommMonoid α] (n : ℤ) : α →+ α

Multiplication by an integer n on a commutative additive group, considered as an additive group homomorphism.

Equations

• zsmulAddGroupHom n = { toZeroHom := { toFun := fun (x : α) => n • x, map_zero' := ⋯ }, map_add' := ⋯ }

theorem zsmulAddGroupHom.proof_1 {α : Type u_1} [SubtractionCommMonoid α] (n : ℤ) : n • 0 = 0

@[simp]

theorem zsmulAddGroupHom_apply {α : Type u_1} [SubtractionCommMonoid α] (n : ℤ) : ∀ (x : α), (zsmulAddGroupHom n) x = n • x

@[simp]

theorem zpowGroupHom_apply {α : Type u_1} [DivisionCommMonoid α] (n : ℤ) : ∀ (x : α), (zpowGroupHom n) x = x ^ n

def zpowGroupHom {α : Type u_1} [DivisionCommMonoid α] (n : ℤ) : α →* α

The n-th power map (for an integer n) on a commutative group, considered as a group homomorphism.

Equations

• zpowGroupHom n = { toOneHom := { toFun := fun (x : α) => x ^ n, map_one' := ⋯ }, map_mul' := ⋯ }