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.Ring.

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.

Monoids

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 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 eq_zero_or_one_of_sq_eq_self {M : Type u} [CancelMonoidWithZero M] {x : M} (hx : x ^ 2 = x) : x = 0 ∨ x = 1

Commutative (additive) monoid

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

abbrev AddCommute.zsmul_add.match_1 (motive : ℤ → Prop) : ∀ (x : ℤ), (∀ (n : ℕ), motive (Int.ofNat n)) → (∀ (n : ℕ), motive (Int.negSucc n)) → motive x

Equations

• ⋯ = ⋯

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

theorem bit0_zsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) : bit0 n • a = n • a + n • a

theorem zpow_bit0 {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) : a ^ bit0 n = a ^ n * a ^ n

theorem bit0_zsmul' {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) : bit0 n • a = n • (a + a)

theorem zpow_bit0' {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) : a ^ bit0 n = (a * 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 bit1_zsmul {G : Type w} [AddGroup G] (a : G) (n : ℤ) : bit1 n • a = n • a + n • a + a

theorem zpow_bit1 {G : Type w} [Group G] (a : G) (n : ℤ) : a ^ bit1 n = a ^ n * a ^ n * a

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