Power operations on monoids and groups

The power operation on monoids and groups. We separate this from group, because it depends on ℕ, which in turn depends on other parts of algebra.

This module contains lemmas about a ^ n and n • a, where n : ℕ or n : ℤ. Further lemmas can be found in Algebra.GroupPower.Lemmas.

The analogous results for groups with zero can be found in Algebra.GroupWithZero.Power.

Notation

• a ^ n is used as notation for Pow.pow a n; in this file n : ℕ or n : ℤ.
• n • a is used as notation for SMul.smul n a; in this file n : ℕ or n : ℤ.

Implementation details

We adopt the convention that 0^0 = 1.

Commutativity

First we prove some facts about SemiconjBy and Commute. They do not require any theory about pow and/or nsmul and will be useful later in this file.

@[simp]

theorem ite_nsmul {M : Type u} [SMul ℕ M] (P : Prop) [Decidable P] (a : M) (b : ℕ) (c : ℕ) : (if P then b else c) • a = if P then b • a else c • a

@[simp]

theorem pow_ite {M : Type u} [Pow M ℕ] (P : Prop) [Decidable P] (a : M) (b : ℕ) (c : ℕ) : (a ^ if P then b else c) = if P then a ^ b else a ^ c

@[simp]

theorem nsmul_ite {M : Type u} [SMul ℕ M] (P : Prop) [Decidable P] (a : M) (b : M) (c : ℕ) : (c • if P then a else b) = if P then c • a else c • b

@[simp]

theorem ite_pow {M : Type u} [Pow M ℕ] (P : Prop) [Decidable P] (a : M) (b : M) (c : ℕ) : (if P then a else b) ^ c = if P then a ^ c else b ^ c

Monoids

theorem nsmul_zero {A : Type y} [AddMonoid A] (n : ℕ) : n • 0 = 0

@[simp]

theorem one_nsmul {A : Type y} [AddMonoid A] (a : A) : 1 • a = a

theorem add_nsmul {A : Type y} [AddMonoid A] (a : A) (m : ℕ) (n : ℕ) : (m + n) • a = m • a + n • a

@[simp]

theorem one_pow {M : Type u} [Monoid M] (n : ℕ) : 1 ^ n = 1

@[simp]

theorem pow_one {M : Type u} [Monoid M] (a : M) : a ^ 1 = a

theorem two_nsmul {M : Type u} [AddMonoid M] (a : M) : 2 • a = a + a

theorem pow_two {M : Type u} [Monoid M] (a : M) : a ^ 2 = a * a

Note that most of the lemmas about powers of two refer to it as sq.

theorem sq {M : Type u} [Monoid M] (a : M) : a ^ 2 = a * a

Alias of pow_two.

---

Note that most of the lemmas about powers of two refer to it as sq.

theorem three'_nsmul {M : Type u} [AddMonoid M] (a : M) : 3 • a = a + a + a

theorem pow_three' {M : Type u} [Monoid M] (a : M) : a ^ 3 = a * a * a

theorem three_nsmul {M : Type u} [AddMonoid M] (a : M) : 3 • a = a + (a + a)

theorem pow_three {M : Type u} [Monoid M] (a : M) : a ^ 3 = a * (a * a)

theorem pow_add {M : Type u} [Monoid M] (a : M) (m : ℕ) (n : ℕ) : a ^ (m + n) = a ^ m * a ^ n

theorem mul_nsmul {M : Type u} [AddMonoid M] (a : M) (m : ℕ) (n : ℕ) : (m * n) • a = n • m • a

theorem pow_mul {M : Type u} [Monoid M] (a : M) (m : ℕ) (n : ℕ) : a ^ (m * n) = (a ^ m) ^ n

theorem mul_nsmul' {M : Type u} [AddMonoid M] (a : M) (m : ℕ) (n : ℕ) : (m * n) • a = m • n • a

theorem pow_mul' {M : Type u} [Monoid M] (a : M) (m : ℕ) (n : ℕ) : a ^ (m * n) = (a ^ n) ^ m

theorem AddCommute.add_nsmul {M : Type u} [AddMonoid M] {a : M} {b : M} (h : AddCommute a b) (n : ℕ) : n • (a + b) = n • a + n • b

theorem Commute.mul_pow {M : Type u} [Monoid M] {a : M} {b : M} (h : Commute a b) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n

theorem nsmul_add_comm' {M : Type u} [AddMonoid M] (a : M) (n : ℕ) : n • a + a = a + n • a

theorem pow_mul_comm' {M : Type u} [Monoid M] (a : M) (n : ℕ) : a ^ n * a = a * a ^ n

theorem boole_nsmul {M : Type u} [AddMonoid M] (P : Prop) [Decidable P] (a : M) : (if P then 1 else 0) • a = if P then a else 0

theorem pow_boole {M : Type u} [Monoid M] (P : Prop) [Decidable P] (a : M) : (a ^ if P then 1 else 0) = if P then a else 1

theorem nsmul_left_comm {M : Type u} [AddMonoid M] (a : M) (m : ℕ) (n : ℕ) : n • m • a = m • n • a

theorem pow_right_comm {M : Type u} [Monoid M] (a : M) (m : ℕ) (n : ℕ) : (a ^ m) ^ n = (a ^ n) ^ m

theorem nsmul_add_sub_nsmul {M : Type u} [AddMonoid M] (a : M) {m : ℕ} {n : ℕ} (h : m ≤ n) : m • a + (n - m) • a = n • a

theorem pow_mul_pow_sub {M : Type u} [Monoid M] (a : M) {m : ℕ} {n : ℕ} (h : m ≤ n) : a ^ m * a ^ (n - m) = a ^ n

theorem sub_nsmul_nsmul_add {M : Type u} [AddMonoid M] (a : M) {m : ℕ} {n : ℕ} (h : m ≤ n) : (n - m) • a + m • a = n • a

theorem pow_sub_mul_pow {M : Type u} [Monoid M] (a : M) {m : ℕ} {n : ℕ} (h : m ≤ n) : a ^ (n - m) * a ^ m = a ^ n

theorem nsmul_eq_mod_nsmul {M : Type u_2} [AddMonoid M] {x : M} (m : ℕ) {n : ℕ} (h : n • x = 0) : m • x = (m % n) • x

If n • x = 0, then m • x is the same as (m % n) • x

theorem pow_eq_pow_mod {M : Type u_2} [Monoid M] {x : M} (m : ℕ) {n : ℕ} (h : x ^ n = 1) : x ^ m = x ^ (m % n)

If x ^ n = 1, then x ^ m is the same as x ^ (m % n)

theorem nsmul_add_comm {M : Type u} [AddMonoid M] (a : M) (m : ℕ) (n : ℕ) : m • a + n • a = n • a + m • a

theorem pow_mul_comm {M : Type u} [Monoid M] (a : M) (m : ℕ) (n : ℕ) : a ^ m * a ^ n = a ^ n * a ^ m

theorem bit0_nsmul {M : Type u} [AddMonoid M] (a : M) (n : ℕ) : bit0 n • a = n • a + n • a

theorem pow_bit0 {M : Type u} [Monoid M] (a : M) (n : ℕ) : a ^ bit0 n = a ^ n * a ^ n

theorem bit1_nsmul {M : Type u} [AddMonoid M] (a : M) (n : ℕ) : bit1 n • a = n • a + n • a + a

theorem pow_bit1 {M : Type u} [Monoid M] (a : M) (n : ℕ) : a ^ bit1 n = a ^ n * a ^ n * a

theorem bit0_nsmul' {M : Type u} [AddMonoid M] (a : M) (n : ℕ) : bit0 n • a = n • (a + a)

theorem pow_bit0' {M : Type u} [Monoid M] (a : M) (n : ℕ) : a ^ bit0 n = (a * a) ^ n

theorem bit1_nsmul' {M : Type u} [AddMonoid M] (a : M) (n : ℕ) : bit1 n • a = n • (a + a) + a

theorem pow_bit1' {M : Type u} [Monoid M] (a : M) (n : ℕ) : a ^ bit1 n = (a * a) ^ n * a

theorem nsmul_add_nsmul_eq_zero {M : Type u} [AddMonoid M] {a : M} {b : M} (n : ℕ) (h : a + b = 0) : n • a + n • b = 0

theorem pow_mul_pow_eq_one {M : Type u} [Monoid M] {a : M} {b : M} (n : ℕ) (h : a * b = 1) : a ^ n * b ^ n = 1

theorem dvd_pow {M : Type u} [Monoid M] {x : M} {y : M} (hxy : x ∣ y) {n : ℕ} : n ≠ 0 → x ∣ y ^ n

theorem Dvd.dvd.pow {M : Type u} [Monoid M] {x : M} {y : M} (hxy : x ∣ y) {n : ℕ} : n ≠ 0 → x ∣ y ^ n

Alias of dvd_pow.

theorem dvd_pow_self {M : Type u} [Monoid M] (a : M) {n : ℕ} (hn : n ≠ 0) : a ∣ a ^ n

Commutative (additive) monoid

theorem nsmul_add {M : Type u} [AddCommMonoid M] (a : M) (b : M) (n : ℕ) : n • (a + b) = n • a + n • b

theorem mul_pow {M : Type u} [CommMonoid M] (a : M) (b : M) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n

def nsmulAddMonoidHom {M : Type u} [AddCommMonoid M] (n : ℕ) : M →+ M

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 : M), n • (a + b) = n • a + n • b) }

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

@[simp]

theorem powMonoidHom_apply {M : Type u} [CommMonoid M] (n : ℕ) : ∀ (x : M), ↑(powMonoidHom n) x = x ^ n

@[simp]

theorem nsmulAddMonoidHom_apply {M : Type u} [AddCommMonoid M] (n : ℕ) : ∀ (x : M), ↑(nsmulAddMonoidHom n) x = n • x

def powMonoidHom {M : Type u} [CommMonoid M] (n : ℕ) : M →* M

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 : M), (a * b) ^ n = a ^ n * b ^ n) }

@[simp]

theorem one_zsmul {G : Type w} [SubNegMonoid G] (a : G) : 1 • a = a

@[simp]

theorem zpow_one {G : Type w} [DivInvMonoid G] (a : G) : a ^ 1 = a

theorem two_zsmul {G : Type w} [SubNegMonoid G] (a : G) : 2 • a = a + a

theorem zpow_two {G : Type w} [DivInvMonoid G] (a : G) : a ^ 2 = a * a

theorem neg_one_zsmul {G : Type w} [SubNegMonoid G] (x : G) : -1 • x = -x

theorem zpow_neg_one {G : Type w} [DivInvMonoid G] (x : G) : x ^ (-1) = x⁻¹

theorem zsmul_neg_coe_of_pos {G : Type w} [SubNegMonoid G] (a : G) {n : ℕ} : 0 < n → -↑n • a = -(n • a)

abbrev zsmul_neg_coe_of_pos.match_1 (motive : (x : ℕ) → 0 < x → Prop) : (x : ℕ) → (x_1 : 0 < x) → ((n : ℕ) → (x : 0 < n + 1) → motive (Nat.succ n) x) → motive x x_1

Equations

• One or more equations did not get rendered due to their size.

theorem zpow_neg_coe_of_pos {G : Type w} [DivInvMonoid G] (a : G) {n : ℕ} : 0 < n → a ^ (-↑n) = (a ^ n)⁻¹

@[simp]

theorem neg_nsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℕ) : n • -a = -(n • a)

abbrev neg_nsmul.match_1 (motive : ℕ → Prop) : (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive (Nat.succ n)) → motive x

Equations

• neg_nsmul.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n

@[simp]

theorem inv_pow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℕ) : a⁻¹ ^ n = (a ^ n)⁻¹

theorem zsmul_zero {α : Type u_1} [SubtractionMonoid α] (n : ℤ) : n • 0 = 0

abbrev zsmul_zero.match_1 (motive : ℤ → Prop) : (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x

Equations

• zsmul_zero.match_1 motive x h_1 h_2 = Int.casesOn x (fun a => h_1 a) fun a => h_2 a

@[simp]

theorem one_zpow {α : Type u_1} [DivisionMonoid α] (n : ℤ) : 1 ^ n = 1

@[simp]

theorem neg_zsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) : -n • a = -(n • a)

abbrev neg_zsmul.match_1 (motive : ℤ → Prop) : (x : ℤ) → ((n : ℕ) → motive (Int.ofNat (Nat.succ n))) → (Unit → motive (Int.ofNat 0)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x

Equations

• neg_zsmul.match_1 motive x h_1 h_2 h_3 = Int.casesOn x (fun a => Nat.casesOn a (h_2 ()) fun n => h_1 n) fun a => h_3 a

@[simp]

theorem zpow_neg {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) : a ^ (-n) = (a ^ n)⁻¹

theorem neg_one_zsmul_add {α : Type u_1} [SubtractionMonoid α] (a : α) (b : α) : -1 • (a + b) = -1 • b + -1 • a

theorem mul_zpow_neg_one {α : Type u_1} [DivisionMonoid α] (a : α) (b : α) : (a * b) ^ (-1) = b ^ (-1) * a ^ (-1)

theorem zsmul_neg {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) : n • -a = -(n • a)

theorem inv_zpow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) : a⁻¹ ^ n = (a ^ n)⁻¹

@[simp]

theorem zsmul_neg' {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) : n • -a = -n • a

@[simp]

theorem inv_zpow' {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) : a⁻¹ ^ n = a ^ (-n)

theorem nsmul_zero_sub {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℕ) : n • (0 - a) = 0 - n • a

theorem one_div_pow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n

theorem zsmul_zero_sub {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) : n • (0 - a) = 0 - n • a

theorem one_div_zpow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) : (1 / a) ^ n = 1 / a ^ n

theorem AddCommute.zsmul_add {α : Type u_1} [SubtractionMonoid α] {a : α} {b : α} (h : AddCommute a b) (i : ℤ) : i • (a + b) = i • a + i • b

theorem Commute.mul_zpow {α : Type u_1} [DivisionMonoid α] {a : α} {b : α} (h : Commute a b) (i : ℤ) : (a * b) ^ i = a ^ i * b ^ i

theorem zsmul_add {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (n : ℤ) : n • (a + b) = n • a + n • b

theorem mul_zpow {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (n : ℤ) : (a * b) ^ n = a ^ n * b ^ n

@[simp]

theorem nsmul_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (n : ℕ) : n • (a - b) = n • a - n • b

@[simp]

theorem div_pow {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (n : ℕ) : (a / b) ^ n = a ^ n / b ^ n

@[simp]

theorem zsmul_sub {α : Type u_1} [SubtractionCommMonoid α] (a : α) (b : α) (n : ℤ) : n • (a - b) = n • a - n • b

@[simp]

theorem div_zpow {α : Type u_1} [DivisionCommMonoid α] (a : α) (b : α) (n : ℤ) : (a / b) ^ n = a ^ n / b ^ n

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

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) }

@[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) }

theorem sub_nsmul {G : Type w} [AddGroup G] (a : G) {m : ℕ} {n : ℕ} (h : n ≤ m) : (m - n) • a = m • a + -(n • a)

theorem pow_sub {G : Type w} [Group G] (a : G) {m : ℕ} {n : ℕ} (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹

theorem nsmul_neg_comm {G : Type w} [AddGroup G] (a : G) (m : ℕ) (n : ℕ) : m • -a + n • a = n • a + m • -a

theorem pow_inv_comm {G : Type w} [Group G] (a : G) (m : ℕ) (n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m

theorem sub_nsmul_neg {G : Type w} [AddGroup G] (a : G) {m : ℕ} {n : ℕ} (h : n ≤ m) : (m - n) • -a = -(m • a) + n • a

theorem inv_pow_sub {G : Type w} [Group G] (a : G) {m : ℕ} {n : ℕ} (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

theorem pow_dvd_pow {R : Type u₁} [Monoid R] (a : R) {m : ℕ} {n : ℕ} (h : m ≤ n) : a ^ m ∣ a ^ n

theorem ofAdd_nsmul {A : Type y} [AddMonoid A] (x : A) (n : ℕ) : ↑Multiplicative.ofAdd (n • x) = ↑Multiplicative.ofAdd x ^ n

theorem ofAdd_zsmul {A : Type y} [SubNegMonoid A] (x : A) (n : ℤ) : ↑Multiplicative.ofAdd (n • x) = ↑Multiplicative.ofAdd x ^ n

theorem ofMul_pow {A : Type y} [Monoid A] (x : A) (n : ℕ) : ↑Additive.ofMul (x ^ n) = n • ↑Additive.ofMul x

theorem ofMul_zpow {G : Type w} [DivInvMonoid G] (x : G) (n : ℤ) : ↑Additive.ofMul (x ^ n) = n • ↑Additive.ofMul x

@[simp]

theorem AddSemiconjBy.zsmul_right {G : Type w} [AddGroup G] {a : G} {x : G} {y : G} (h : AddSemiconjBy a x y) (m : ℤ) : AddSemiconjBy a (m • x) (m • y)

@[simp]

theorem SemiconjBy.zpow_right {G : Type w} [Group G] {a : G} {x : G} {y : G} (h : SemiconjBy a x y) (m : ℤ) : SemiconjBy a (x ^ m) (y ^ m)

@[simp]

theorem AddCommute.zsmul_right {G : Type w} [AddGroup G] {a : G} {b : G} (h : AddCommute a b) (m : ℤ) : AddCommute a (m • b)

@[simp]

theorem Commute.zpow_right {G : Type w} [Group G] {a : G} {b : G} (h : Commute a b) (m : ℤ) : Commute a (b ^ m)

@[simp]

theorem AddCommute.zsmul_left {G : Type w} [AddGroup G] {a : G} {b : G} (h : AddCommute a b) (m : ℤ) : AddCommute (m • a) b

@[simp]

theorem Commute.zpow_left {G : Type w} [Group G] {a : G} {b : G} (h : Commute a b) (m : ℤ) : Commute (a ^ m) b

theorem AddCommute.zsmul_zsmul {G : Type w} [AddGroup G] {a : G} {b : G} (h : AddCommute a b) (m : ℤ) (n : ℤ) : AddCommute (m • a) (n • b)

theorem Commute.zpow_zpow {G : Type w} [Group G] {a : G} {b : G} (h : Commute a b) (m : ℤ) (n : ℤ) : Commute (a ^ m) (b ^ n)

theorem AddCommute.self_zsmul {G : Type w} [AddGroup G] (a : G) (n : ℤ) : AddCommute a (n • a)

theorem Commute.self_zpow {G : Type w} [Group G] (a : G) (n : ℤ) : Commute a (a ^ n)

theorem AddCommute.zsmul_self {G : Type w} [AddGroup G] (a : G) (n : ℤ) : AddCommute (n • a) a

theorem Commute.zpow_self {G : Type w} [Group G] (a : G) (n : ℤ) : Commute (a ^ n) a

theorem AddCommute.zsmul_zsmul_self {G : Type w} [AddGroup G] (a : G) (m : ℤ) (n : ℤ) : AddCommute (m • a) (n • a)

theorem Commute.zpow_zpow_self {G : Type w} [Group G] (a : G) (m : ℤ) (n : ℤ) : Commute (a ^ m) (a ^ n)