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

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.

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⁻¹
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 < xProp) :
∀ (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)
Instances For
    theorem zpow_neg_coe_of_pos {G : Type w} [DivInvMonoid G] (a : G) {n : } :
    0 < na ^ (-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 : ), (Unitmotive 0)(∀ (n : ), motive (Nat.succ n))motive x
    Equations
    • (_ : motive x) = (_ : motive x)
    Instances For
      @[simp]
      theorem inv_pow {α : Type u_1} [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
      • (_ : motive x) = (_ : motive x)
      Instances For
        theorem zsmul_zero {α : Type u_1} [SubtractionMonoid α] (n : ) :
        n 0 = 0
        @[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)))(Unitmotive (Int.ofNat 0))(∀ (n : ), motive (Int.negSucc n))motive x
        Equations
        • (_ : motive x) = (_ : motive x)
        Instances For
          @[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)
          Instances For
            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
            theorem add_one_zsmul {G : Type w} [AddGroup G] (a : G) (n : ) :
            (n + 1) a = n a + a
            abbrev add_one_zsmul.match_1 (motive : Prop) :
            ∀ (x : ), (∀ (n : ), motive (Int.ofNat n))(Unitmotive (Int.negSucc 0))(∀ (n : ), motive (Int.negSucc (Nat.succ n)))motive x
            Equations
            • (_ : motive x) = (_ : motive x)
            Instances For
              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 zpow_eq_zpow_emod {G : Type w} [Group G] {x : G} (m : ) {n : } (h : x ^ n = 1) :
              x ^ m = x ^ (m % n)
              theorem zpow_eq_zpow_emod' {G : Type w} [Group G] {x : G} (m : ) {n : } (h : x ^ n = 1) :
              x ^ m = x ^ (m % n)
              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 : GProp} (h_one : P 0) (h_mul : ∀ (a : G), P aP (g + a)) (h_inv : ∀ (a : G), P aP (-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 : GProp} (h_one : P 1) (h_mul : ∀ (a : G), P aP (g * a)) (h_inv : ∀ (a : G), P aP (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 : GProp} (h_one : P 0) (h_mul : ∀ (a : G), P aP (a + g)) (h_inv : ∀ (a : G), P aP (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 : GProp} (h_one : P 1) (h_mul : ∀ (a : G), P aP (a * g)) (h_inv : ∀ (a : G), P aP (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)