Documentation

Mathlib.Algebra.GroupPower.Basic

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 #

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

theorem nsmul_zero {A : Type y} [inst : AddMonoid A] (n : ) :
n 0 = 0
@[simp]
theorem one_nsmul {A : Type y} [inst : AddMonoid A] (a : A) :
1 a = a
theorem add_nsmul {A : Type y} [inst : AddMonoid A] (a : A) (m : ) (n : ) :
(m + n) a = m a + n a
@[simp]
theorem one_pow {M : Type u} [inst : Monoid M] (n : ) :
1 ^ n = 1
@[simp]
theorem pow_one {M : Type u} [inst : Monoid M] (a : M) :
a ^ 1 = a
theorem two_nsmul {M : Type u} [inst : AddMonoid M] (a : M) :
2 a = a + a
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.

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

Alias of pow_two.

theorem pow_three' {M : Type u} [inst : Monoid M] (a : M) :
a ^ 3 = a * a * a
theorem pow_three {M : Type u} [inst : Monoid M] (a : M) :
a ^ 3 = a * (a * a)
theorem pow_add {M : Type u} [inst : Monoid M] (a : M) (m : ) (n : ) :
a ^ (m + n) = a ^ m * a ^ n
theorem mul_nsmul {M : Type u} [inst : AddMonoid M] (a : M) (m : ) (n : ) :
(m * n) a = n m a
theorem pow_mul {M : Type u} [inst : Monoid M] (a : M) (m : ) (n : ) :
a ^ (m * n) = (a ^ m) ^ n
theorem mul_nsmul' {M : Type u} [inst : AddMonoid M] (a : M) (m : ) (n : ) :
(m * n) a = m n a
theorem pow_mul' {M : Type u} [inst : Monoid M] (a : M) (m : ) (n : ) :
a ^ (m * n) = (a ^ n) ^ m
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
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
theorem nsmul_add_comm' {M : Type u} [inst : AddMonoid M] (a : M) (n : ) :
n a + a = a + n a
theorem pow_mul_comm' {M : Type u} [inst : Monoid M] (a : M) (n : ) :
a ^ n * a = a * a ^ n
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
theorem nsmul_left_comm {M : Type u} [inst : AddMonoid M] (a : M) (m : ) (n : ) :
n m a = m n a
theorem pow_right_comm {M : Type u} [inst : Monoid M] (a : M) (m : ) (n : ) :
(a ^ m) ^ n = (a ^ n) ^ m
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
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
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
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
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

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)

theorem nsmul_add_comm {M : Type u} [inst : AddMonoid M] (a : M) (m : ) (n : ) :
m a + n a = n a + m a
theorem pow_mul_comm {M : Type u} [inst : Monoid M] (a : M) (m : ) (n : ) :
a ^ m * a ^ n = a ^ n * a ^ m
theorem bit0_nsmul {M : Type u} [inst : AddMonoid M] (a : M) (n : ) :
bit0 n a = n a + n a
theorem pow_bit0 {M : Type u} [inst : Monoid M] (a : M) (n : ) :
a ^ bit0 n = a ^ n * a ^ n
theorem bit1_nsmul {M : Type u} [inst : AddMonoid M] (a : M) (n : ) :
bit1 n a = n a + n a + a
theorem pow_bit1 {M : Type u} [inst : Monoid M] (a : M) (n : ) :
a ^ bit1 n = a ^ n * a ^ n * a
theorem bit0_nsmul' {M : Type u} [inst : AddMonoid M] (a : M) (n : ) :
bit0 n a = n (a + a)
theorem pow_bit0' {M : Type u} [inst : Monoid M] (a : M) (n : ) :
a ^ bit0 n = (a * a) ^ n
theorem bit1_nsmul' {M : Type u} [inst : AddMonoid M] (a : M) (n : ) :
bit1 n a = n (a + a) + a
theorem pow_bit1' {M : Type u} [inst : Monoid M] (a : M) (n : ) :
a ^ bit1 n = (a * a) ^ n * a
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
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
theorem dvd_pow {M : Type u} [inst : Monoid M] {x : M} {y : M} (hxy : x y) {n : } :
n 0x y ^ n
theorem Dvd.dvd.pow {M : Type u} [inst : Monoid M] {x : M} {y : M} (hxy : x y) {n : } :
n 0x y ^ n

Alias of dvd_pow.

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

Commutative (additive) monoid #

theorem nsmul_add {M : Type u} [inst : AddCommMonoid M] (a : M) (b : M) (n : ) :
n (a + b) = n a + n b
theorem mul_pow {M : Type u} [inst : CommMonoid M] (a : M) (b : M) (n : ) :
(a * b) ^ n = a ^ n * b ^ n
def nsmulAddMonoidHom.proof_1 {M : Type u_1} [inst : AddCommMonoid M] (n : ) :
n 0 = 0
Equations
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
def nsmulAddMonoidHom.proof_2 {M : Type u_1} [inst : AddCommMonoid M] (n : ) (a : M) (b : M) :
n (a + b) = n a + n b
Equations
@[simp]
theorem nsmulAddMonoidHom_apply {M : Type u} [inst : AddCommMonoid M] (n : ) :
∀ (x : M), ↑(nsmulAddMonoidHom n) x = n x
@[simp]
theorem powMonoidHom_apply {M : Type u} [inst : CommMonoid M] (n : ) :
∀ (x : M), ↑(powMonoidHom n) x = x ^ n
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) }
@[simp]
theorem one_zsmul {G : Type w} [inst : SubNegMonoid G] (a : G) :
1 a = a
@[simp]
theorem zpow_one {G : Type w} [inst : DivInvMonoid G] (a : G) :
a ^ 1 = a
theorem two_zsmul {G : Type w} [inst : SubNegMonoid G] (a : G) :
2 a = a + a
theorem zpow_two {G : Type w} [inst : DivInvMonoid G] (a : G) :
a ^ 2 = a * a
theorem neg_one_zsmul {G : Type w} [inst : SubNegMonoid G] (x : G) :
-1 x = -x
theorem zpow_neg_one {G : Type w} [inst : DivInvMonoid G] (x : G) :
x ^ (-1) = x⁻¹
abbrev zsmul_neg_coe_of_pos.match_1 (motive : (x : ) → 0 < xProp) :
(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 zsmul_neg_coe_of_pos {G : Type w} [inst : SubNegMonoid G] (a : G) {n : } :
0 < n-n a = -(n a)
theorem zpow_neg_coe_of_pos {G : Type w} [inst : DivInvMonoid G] (a : G) {n : } :
0 < na ^ (-n) = (a ^ n)⁻¹
@[simp]
theorem neg_nsmul {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ) :
n -a = -(n a)
abbrev neg_nsmul.match_1 (motive : Prop) :
(x : ) → (Unitmotive 0) → ((n : ) → motive (Nat.succ n)) → motive x
Equations
@[simp]
theorem inv_pow {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ) :
a⁻¹ ^ n = (a ^ n)⁻¹
abbrev zsmul_zero.match_1 (motive : Prop) :
(x : ) → ((n : ) → motive (Int.ofNat n)) → ((n : ) → motive (Int.negSucc n)) → motive x
Equations
theorem zsmul_zero {α : Type u_1} [inst : SubtractionMonoid α] (n : ) :
n 0 = 0
@[simp]
theorem one_zpow {α : Type u_1} [inst : DivisionMonoid α] (n : ) :
1 ^ n = 1
@[simp]
theorem neg_zsmul {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ) :
-n a = -(n a)
abbrev neg_zsmul.match_1 (motive : Prop) :
(x : ) → ((n : ) → motive (Int.ofNat (Nat.succ n))) → (Unitmotive (Int.ofNat 0)) → ((n : ) → motive (Int.negSucc n)) → motive x
Equations
@[simp]
theorem zpow_neg {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ) :
a ^ (-n) = (a ^ n)⁻¹
theorem neg_one_zsmul_add {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (b : α) :
-1 (a + b) = -1 b + -1 a
theorem mul_zpow_neg_one {α : Type u_1} [inst : DivisionMonoid α] (a : α) (b : α) :
(a * b) ^ (-1) = b ^ (-1) * a ^ (-1)
theorem zsmul_neg {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ) :
n -a = -(n a)
theorem inv_zpow {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ) :
a⁻¹ ^ n = (a ^ n)⁻¹
@[simp]
theorem zsmul_neg' {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ) :
n -a = -n a
@[simp]
theorem inv_zpow' {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ) :
a⁻¹ ^ n = a ^ (-n)
theorem nsmul_zero_sub {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ) :
n (0 - a) = 0 - n a
theorem one_div_pow {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ) :
(1 / a) ^ n = 1 / a ^ n
theorem zsmul_zero_sub {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ) :
n (0 - a) = 0 - n a
theorem one_div_zpow {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ) :
(1 / a) ^ n = 1 / a ^ n
theorem AddCommute.zsmul_add {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} (h : AddCommute a b) (i : ) :
i (a + b) = i a + i b
theorem Commute.mul_zpow {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} (h : Commute a b) (i : ) :
(a * b) ^ i = a ^ i * b ^ i
theorem zsmul_add {α : Type u_1} [inst : SubtractionCommMonoid α] (a : α) (b : α) (n : ) :
n (a + b) = n a + n b
theorem mul_zpow {α : Type u_1} [inst : DivisionCommMonoid α] (a : α) (b : α) (n : ) :
(a * b) ^ n = a ^ n * b ^ n
@[simp]
theorem nsmul_sub {α : Type u_1} [inst : SubtractionCommMonoid α] (a : α) (b : α) (n : ) :
n (a - b) = n a - n b
@[simp]
theorem div_pow {α : Type u_1} [inst : DivisionCommMonoid α] (a : α) (b : α) (n : ) :
(a / b) ^ n = a ^ n / b ^ n
@[simp]
theorem zsmul_sub {α : Type u_1} [inst : SubtractionCommMonoid α] (a : α) (b : α) (n : ) :
n (a - b) = n a - n b
@[simp]
theorem div_zpow {α : Type u_1} [inst : DivisionCommMonoid α] (a : α) (b : α) (n : ) :
(a / b) ^ n = a ^ n / b ^ n
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
def zsmulAddGroupHom.proof_1 {α : Type u_1} [inst : SubtractionCommMonoid α] (n : ) :
n 0 = 0
Equations
def zsmulAddGroupHom.proof_2 {α : Type u_1} [inst : SubtractionCommMonoid α] (n : ) (a : α) (b : α) :
n (a + b) = n a + n b
Equations
@[simp]
theorem zpowGroupHom_apply {α : Type u_1} [inst : DivisionCommMonoid α] (n : ) :
∀ (x : α), ↑(zpowGroupHom n) x = x ^ n
@[simp]
theorem zsmulAddGroupHom_apply {α : Type u_1} [inst : SubtractionCommMonoid α] (n : ) :
∀ (x : α), ↑(zsmulAddGroupHom n) x = n x
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) }
theorem sub_nsmul {G : Type w} [inst : AddGroup G] (a : G) {m : } {n : } (h : n m) :
(m - n) a = m a + -(n a)
theorem pow_sub {G : Type w} [inst : Group G] (a : G) {m : } {n : } (h : n m) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
theorem nsmul_neg_comm {G : Type w} [inst : AddGroup G] (a : G) (m : ) (n : ) :
m -a + n a = n a + m -a
theorem pow_inv_comm {G : Type w} [inst : Group G] (a : G) (m : ) (n : ) :
a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m
theorem sub_nsmul_neg {G : Type w} [inst : AddGroup G] (a : G) {m : } {n : } (h : n m) :
(m - n) -a = -(m a) + n a
theorem inv_pow_sub {G : Type w} [inst : Group G] (a : G) {m : } {n : } (h : n m) :
a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
theorem pow_dvd_pow {R : Type u₁} [inst : Monoid R] (a : R) {m : } {n : } (h : m n) :
a ^ m a ^ n
theorem ofAdd_nsmul {A : Type y} [inst : AddMonoid A] (x : A) (n : ) :
Multiplicative.ofAdd (n x) = Multiplicative.ofAdd x ^ n
theorem ofAdd_zsmul {A : Type y} [inst : SubNegMonoid A] (x : A) (n : ) :
Multiplicative.ofAdd (n x) = Multiplicative.ofAdd x ^ n
theorem ofMul_pow {A : Type y} [inst : Monoid A] (x : A) (n : ) :
Additive.ofMul (x ^ n) = n Additive.ofMul x
theorem ofMul_zpow {G : Type w} [inst : DivInvMonoid G] (x : G) (n : ) :
Additive.ofMul (x ^ n) = n Additive.ofMul x
@[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)
@[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)
@[simp]
theorem AddCommute.zsmul_right {G : Type w} [inst : AddGroup G] {a : G} {b : G} (h : AddCommute a b) (m : ) :
AddCommute a (m b)
@[simp]
theorem Commute.zpow_right {G : Type w} [inst : Group G] {a : G} {b : G} (h : Commute a b) (m : ) :
Commute a (b ^ m)
@[simp]
theorem AddCommute.zsmul_left {G : Type w} [inst : AddGroup G] {a : G} {b : G} (h : AddCommute a b) (m : ) :
AddCommute (m a) b
@[simp]
theorem Commute.zpow_left {G : Type w} [inst : Group G] {a : G} {b : G} (h : Commute a b) (m : ) :
Commute (a ^ m) b
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)
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)
theorem AddCommute.self_zsmul {G : Type w} [inst : AddGroup G] (a : G) (n : ) :
AddCommute a (n a)
theorem Commute.self_zpow {G : Type w} [inst : Group G] (a : G) (n : ) :
Commute a (a ^ n)
theorem AddCommute.zsmul_self {G : Type w} [inst : AddGroup G] (a : G) (n : ) :
AddCommute (n a) a
theorem Commute.zpow_self {G : Type w} [inst : Group G] (a : G) (n : ) :
Commute (a ^ n) a
theorem AddCommute.zsmul_zsmul_self {G : Type w} [inst : AddGroup G] (a : G) (m : ) (n : ) :
AddCommute (m a) (n a)
theorem Commute.zpow_zpow_self {G : Type w} [inst : Group G] (a : G) (m : ) (n : ) :
Commute (a ^ m) (a ^ n)