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.

ink

@[simp]

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

ink

@[simp]

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

Monoids

ink

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

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

ink

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

Alias of pow_two.

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem nsmul_eq_mod_nsmul {M : Type u_1} [inst : 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

ink

theorem pow_eq_pow_mod {M : Type u_1} [inst : 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)

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

Alias of dvd_pow.

ink

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

Commutative (additive) monoid

ink

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

ink

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

ink

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

Equations

• (_ : n • 0 = 0) = (_ : n • 0 = 0)

ink

def nsmulAddMonoidHom {M : Type u} [inst : 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) }

ink

def nsmulAddMonoidHom.proof_2 {M : Type u_1} [inst : AddCommMonoid M] (n : ℕ) (a : M) (b : M) : n • (a + b) = n • a + n • b

Equations

• (_ : n • (a + b) = n • a + n • b) = (_ : n • (a + b) = n • a + n • b)

ink

@[simp]

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

ink

@[simp]

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

ink

def powMonoidHom {M : Type u} [inst : 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) }

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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.

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

def zsmulAddGroupHom {α : Type u_1} [inst : 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) }

ink

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

Equations

• (_ : n • 0 = 0) = (_ : n • 0 = 0)

ink

def zsmulAddGroupHom.proof_2 {α : Type u_1} [inst : SubtractionCommMonoid α] (n : ℤ) (a : α) (b : α) : n • (a + b) = n • a + n • b

Equations

• (_ : n • (a + b) = n • a + n • b) = (_ : n • (a + b) = n • a + n • b)

ink

@[simp]

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

ink

@[simp]

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

ink

def zpowGroupHom {α : Type u_1} [inst : 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) }

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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