Power as a monoid hom

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' := (_ : n • 0 = 0) }, map_add' := (_ : ∀ (a b : α), n • (a + b) = n • a + n • b) }

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

@[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' := (_ : 1 ^ n = 1) }, map_mul' := (_ : ∀ (a b : α), (a * b) ^ n = a ^ n * b ^ n) }

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' := (_ : n • 0 = 0) }, map_add' := (_ : ∀ (a b : α), n • (a + b) = n • a + n • b) }

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

@[simp]

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

@[simp]

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

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' := (_ : 1 ^ n = 1) }, map_mul' := (_ : ∀ (a b : α), (a * b) ^ n = a ^ n * b ^ n) }