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

@[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⁻¹

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

• (_ : motive x✝ x) = (_ : motive x✝ x)

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

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

• (_ : motive x) = (_ : motive x)

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

• (_ : motive x) = (_ : motive x)

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

• (_ : motive x) = (_ : motive x)

@[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 mul_zsmul' {α : Type u_1} [SubtractionMonoid α] (a : α) (m : ℤ) (n : ℤ) : (m * n) • a = n • m • a

abbrev mul_zsmul'.match_1 (motive : ℤ → ℤ → Prop) : ∀ (x x_1 : ℤ), (∀ (m n : ℕ), motive (Int.ofNat m) (Int.ofNat n)) → (∀ (m n : ℕ), motive (Int.ofNat m) (Int.negSucc n)) → (∀ (m n : ℕ), motive (Int.negSucc m) (Int.ofNat n)) → (∀ (m n : ℕ), motive (Int.negSucc m) (Int.negSucc n)) → motive x x_1

Equations

• (_ : motive x✝ x) = (_ : motive x✝ x)

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

theorem mul_zsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (m : ℤ) (n : ℤ) : (m * n) • a = m • n • a

theorem zpow_mul' {α : Type u_1} [DivisionMonoid α] (a : α) (m : ℤ) (n : ℤ) : a ^ (m * n) = (a ^ n) ^ m

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

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

Equations

• (_ : motive x) = (_ : motive x)

theorem add_one_zsmul {G : Type w} [AddGroup G] (a : G) (n : ℤ) : (n + 1) • a = n • a + a

theorem zpow_add_one {G : Type w} [Group G] (a : G) (n : ℤ) : a ^ (n + 1) = a ^ n * a

theorem sub_one_zsmul {G : Type w} [AddGroup G] (a : G) (n : ℤ) : (n - 1) • a = n • a + -a

theorem zpow_sub_one {G : Type w} [Group G] (a : G) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹

theorem add_zsmul {G : Type w} [AddGroup G] (a : G) (m : ℤ) (n : ℤ) : (m + n) • a = m • a + n • a

theorem zpow_add {G : Type w} [Group G] (a : G) (m : ℤ) (n : ℤ) : a ^ (m + n) = a ^ m * a ^ n

theorem one_add_zsmul {G : Type w} [AddGroup G] (a : G) (n : ℤ) : (1 + n) • a = a + n • a

theorem zpow_one_add {G : Type w} [Group G] (a : G) (n : ℤ) : a ^ (1 + n) = a * a ^ n

theorem add_zsmul_self {G : Type w} [AddGroup G] (a : G) (n : ℤ) : a + n • a = (n + 1) • a

theorem mul_self_zpow {G : Type w} [Group G] (a : G) (n : ℤ) : a * a ^ n = a ^ (n + 1)

theorem add_self_zsmul {G : Type w} [AddGroup G] (a : G) (n : ℤ) : n • a + a = (n + 1) • a

theorem mul_zpow_self {G : Type w} [Group G] (a : G) (n : ℤ) : a ^ n * a = a ^ (n + 1)

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

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

theorem zsmul_add_comm {G : Type w} [AddGroup G] (a : G) (m : ℤ) (n : ℤ) : m • a + n • a = n • a + m • a

theorem zpow_mul_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

theorem zsmul_induction_left {G : Type w} [AddGroup G] {g : G} {P : G → Prop} (h_one : P 0) (h_mul : ∀ (a : G), P a → P (g + a)) (h_inv : ∀ (a : G), P a → P (-g + a)) (n : ℤ) : P (n • g)

To show a property of all multiples of g it suffices to show it is closed under addition by g and -g on the left. For additive subgroups generated by more than one element, see AddSubgroup.closure_induction_left.

theorem zpow_induction_left {G : Type w} [Group G] {g : G} {P : G → Prop} (h_one : P 1) (h_mul : ∀ (a : G), P a → P (g * a)) (h_inv : ∀ (a : G), P a → P (g⁻¹ * a)) (n : ℤ) : P (g ^ n)

To show a property of all powers of g it suffices to show it is closed under multiplication by g and g⁻¹ on the left. For subgroups generated by more than one element, see Subgroup.closure_induction_left.

theorem zsmul_induction_right {G : Type w} [AddGroup G] {g : G} {P : G → Prop} (h_one : P 0) (h_mul : ∀ (a : G), P a → P (a + g)) (h_inv : ∀ (a : G), P a → P (a + -g)) (n : ℤ) : P (n • g)

To show a property of all multiples of g it suffices to show it is closed under addition by g and -g on the right. For additive subgroups generated by more than one element, see AddSubgroup.closure_induction_right.

theorem zpow_induction_right {G : Type w} [Group G] {g : G} {P : G → Prop} (h_one : P 1) (h_mul : ∀ (a : G), P a → P (a * g)) (h_inv : ∀ (a : G), P a → P (a * g⁻¹)) (n : ℤ) : P (g ^ n)

To show a property of all powers of g it suffices to show it is closed under multiplication by g and g⁻¹ on the right. For subgroups generated by more than one element, see Subgroup.closure_induction_right.

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