Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2015 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Robert Y. Lewis
! This file was ported from Lean 3 source module algebra.group_power.basic
! leanprover-community/mathlib commit 9b2660e1b25419042c8da10bf411aa3c67f14383
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Divisibility.Basic
import Mathlib.Algebra.Group.Commute
import Mathlib.Algebra.Group.TypeTags
/-!
# 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`.
-/
universe u v w x y z u₁ u₂
variable { α : Type _ } { M : Type u } { N : Type v } { G : Type w } { H : Type x } { A : Type y } { B : Type z }
{ R : Type u₁ } { S : Type u₂ }
/-!
### 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.
-/
section Pow
variable [ Pow M ℕ ]
@[ simp ]
theorem pow_ite : ∀ {M : Type u} [inst : Pow M ℕ P : Prop ) [inst_1 : Decidable P a : M ) (b c : ℕ ),
(a ^ if P then b else c = if P then a ^ b a ^ c pow_ite ( P : Prop ) [ Decidable P ] ( a : M ) ( b c : ℕ ) :
( a ^ if P then b else c ) = if P then a ^ b else a ^ c := by (a ^ if P then b else c = if P then a ^ b a ^ c split_ifs (a ^ if P then b else c = if P then a ^ b a ^ c <;> (a ^ if P then b else c = if P then a ^ b a ^ c rfl
#align pow_ite pow_ite : ∀ {M : Type u} [inst : Pow M ℕ P : Prop ) [inst_1 : Decidable P a : M ) (b c : ℕ ),
(a ^ if P then b else c = if P then a ^ b a ^ c
@[ simp ]
theorem ite_pow : ∀ {M : Type u} [inst : Pow M ℕ P : Prop ) [inst_1 : Decidable P a b : M ) (c : ℕ ),
(if P then a else b ) ^ c = if P then a ^ c b ^ c ite_pow ( P : Prop ) [ Decidable P ] ( a b : M ) ( c : ℕ ) :
( if P then a else b ) ^ c = if P then a ^ c else b ^ c := by (if P then a else b ) ^ c = if P then a ^ c b ^ c split_ifs (if P then a else b ) ^ c = if P then a ^ c b ^ c <;> (if P then a else b ) ^ c = if P then a ^ c b ^ c rfl
#align ite_pow ite_pow : ∀ {M : Type u} [inst : Pow M ℕ P : Prop ) [inst_1 : Decidable P a b : M ) (c : ℕ ),
(if P then a else b ) ^ c = if P then a ^ c b ^ c
end Pow
/-!
### Monoids
-/
section Monoid
variable [ Monoid M ] [ AddMonoid A ]
theorem nsmul_zero ( n : ℕ ) : n • ( 0 : A ) = 0 := by
induction' n with n ih
· exact zero_nsmul _
· rw [ succ_nsmul , ih , add_zero ]
#align nsmul_zero nsmul_zero
@[ simp ]
theorem one_nsmul ( a : A ) : 1 • a = a := by rw [ succ_nsmul , zero_nsmul , add_zero ]
#align one_nsmul one_nsmul
theorem add_nsmul : ∀ (a : A ) (m n : ℕ ), (m + n • a = m • a + n • a add_nsmul ( a : A ) ( m n : ℕ ) : ( m + n ) • a = m • a + n • a := by
induction m with
| zero => rw [ Nat.zero_add : ∀ (n : ℕ ), 0 + n = n , zero_nsmul , zero_add ]
| succ m ih => rw [ Nat.succ_add , Nat.succ_eq_add_one , succ_nsmul , ih , succ_nsmul , add_assoc ]
#align add_nsmul add_nsmul
-- the attributes are intentionally out of order.
@[ to_additive existing nsmul_zero , simp ]
theorem one_pow : ∀ (n : ℕ ), 1 ^ n = 1 one_pow ( n : ℕ ) : ( 1 : M ) ^ n = 1 := by
induction' n with n ih
· exact pow_zero : ∀ {M : Type ?u.11304} [inst : Monoid M a : M ), a ^ 0 = 1 _
· rw [ pow_succ : ∀ {M : Type ?u.11340} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a * a ^ n , ih , one_mul ]
#align one_pow one_pow
@[ to_additive existing ( attr := simp ) one_nsmul ]
theorem pow_one : ∀ (a : M ), a ^ 1 = a pow_one ( a : M ) : a ^ 1 = a := by rw [ pow_succ : ∀ {M : Type ?u.11675} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a * a ^ n , pow_zero : ∀ {M : Type ?u.11715} [inst : Monoid M a : M ), a ^ 0 = 1 , mul_one ]
#align pow_one pow_one : ∀ {M : Type u} [inst : Monoid M a : M ), a ^ 1 = a
/-- Note that most of the lemmas about powers of two refer to it as `sq`. -/
@[ to_additive two_nsmul ""]
theorem pow_two : ∀ (a : M ), a ^ 2 = a * a pow_two ( a : M ) : a ^ 2 = a * a := by rw [ pow_succ : ∀ {M : Type ?u.12197} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a * a ^ n , pow_one : ∀ {M : Type ?u.12237} [inst : Monoid M a : M ), a ^ 1 = a ]
#align pow_two pow_two
#align two_nsmul two_nsmul
alias pow_two ← sq
#align sq sq
theorem pow_three' : ∀ (a : M ), a ^ 3 = a * a * a pow_three' ( a : M ) : a ^ 3 = a * a * a := by rw [ pow_succ' : ∀ {M : Type ?u.12688} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a ^ n * a , pow_two : ∀ {M : Type ?u.12728} [inst : Monoid M a : M ), a ^ 2 = a * a ]
#align pow_three' pow_three' : ∀ {M : Type u} [inst : Monoid M a : M ), a ^ 3 = a * a * a
theorem pow_three : ∀ (a : M ), a ^ 3 = a * (a * a pow_three ( a : M ) : a ^ 3 = a * ( a * a ) := by rw [ pow_succ : ∀ {M : Type ?u.13165} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a * a ^ n , pow_two : ∀ {M : Type ?u.13205} [inst : Monoid M a : M ), a ^ 2 = a * a a * (a * a = a * (a * a ]
#align pow_three pow_three : ∀ {M : Type u} [inst : Monoid M a : M ), a ^ 3 = a * (a * a
@[ to_additive existing add_nsmul ]
theorem pow_add : ∀ (a : M ) (m n : ℕ ), a ^ (m + n = a ^ m * a ^ n pow_add ( a : M ) ( m n : ℕ ) : a ^ ( m + n ) = a ^ m * a ^ n := by
induction' n with n ih
· rw [ Nat.add_zero : ∀ (n : ℕ ), n + 0 = n , pow_zero : ∀ {M : Type ?u.14777} [inst : Monoid M a : M ), a ^ 0 = 1 , mul_one ]
· rw [ pow_succ' : ∀ {M : Type ?u.14903} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a ^ n * a , ← mul_assoc : ∀ {G : Type ?u.14950} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , ← ih , ← pow_succ' : ∀ {M : Type ?u.15030} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a ^ n * a , Nat.add_assoc : ∀ (n m k : ℕ ), n + m + k = n + (m + k ]
#align pow_add pow_add : ∀ {M : Type u} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m + n = a ^ m * a ^ n
@[ to_additive mul_nsmul ]
theorem pow_mul : ∀ {M : Type u} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m * n = (a ^ m ^ n pow_mul ( a : M ) ( m n : ℕ ) : a ^ ( m * n ) = ( a ^ m ) ^ n := by
a ^ (m * n = (a ^ m ^ n induction' n with n ih
a ^ (m * n = (a ^ m ^ n · rw [ Nat.mul_zero : ∀ (n : ℕ ), n * 0 = 0 , pow_zero : ∀ {M : Type ?u.16546} [inst : Monoid M a : M ), a ^ 0 = 1 , pow_zero : ∀ {M : Type ?u.16590} [inst : Monoid M a : M ), a ^ 0 = 1 ]
a ^ (m * n = (a ^ m ^ n · rw [ Nat.mul_succ , pow_add : ∀ {M : Type ?u.16628} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m + n = a ^ m * a ^ n , pow_succ' : ∀ {M : Type ?u.16665} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a ^ n * a , ih ]
-- Porting note: we are taking the opportunity to swap the names `mul_nsmul` and `mul_nsmul'`
-- using #align, so that in mathlib4 they will match the multiplicative ones.
#align pow_mul pow_mul : ∀ {M : Type u} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m * n = (a ^ m ^ n
#align mul_nsmul' mul_nsmul
@[ to_additive mul_nsmul' ]
theorem pow_mul' : ∀ {M : Type u} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m * n = (a ^ n ^ m pow_mul' ( a : M ) ( m n : ℕ ) : a ^ ( m * n ) = ( a ^ n ) ^ m := by a ^ (m * n = (a ^ n ^ m rw [ a ^ (m * n = (a ^ n ^ m Nat.mul_comm : ∀ (n m : ℕ ), n * m = m * n , a ^ (n * m = (a ^ n ^ m a ^ (m * n = (a ^ n ^ m pow_mul : ∀ {M : Type ?u.18196} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m * n = (a ^ m ^ n (a ^ n ^ m = (a ^ n ^ m ]
#align pow_mul' pow_mul' : ∀ {M : Type u} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m * n = (a ^ n ^ m
#align mul_nsmul mul_nsmul'
@[ to_additive ]
theorem Commute.mul_pow : ∀ {a b : M }, Commute a b ∀ (n : ℕ ), (a * b ^ n = a ^ n * b ^ n Commute.mul_pow { a b : M } ( h : Commute : {S : Type ?u.18307} → [inst : Mul S S → S → Prop a b ) ( n : ℕ ) : ( a * b ) ^ n = a ^ n * b ^ n := by
induction' n with n ih
· rw [ pow_zero : ∀ {M : Type ?u.19922} [inst : Monoid M a : M ), a ^ 0 = 1 , pow_zero : ∀ {M : Type ?u.19966} [inst : Monoid M a : M ), a ^ 0 = 1 , pow_zero : ∀ {M : Type ?u.19993} [inst : Monoid M a : M ), a ^ 0 = 1 , one_mul ]
· simp only [ pow_succ : ∀ {M : Type ?u.20107} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a * a ^ n , ih , ← mul_assoc : ∀ {G : Type ?u.20124} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , ( h . pow_left n ). right_comm ]
#align commute.mul_pow Commute.mul_pow
#align add_commute.add_nsmul AddCommute.add_nsmul
@[ to_additive ]
theorem pow_mul_comm' : ∀ (a : M ) (n : ℕ ), a ^ n * a = a * a ^ n pow_mul_comm' ( a : M ) ( n : ℕ ) : a ^ n * a = a * a ^ n :=
Commute.pow_self a n
#align pow_mul_comm' pow_mul_comm' : ∀ {M : Type u} [inst : Monoid M a : M ) (n : ℕ ), a ^ n * a = a * a ^ n
#align nsmul_add_comm' nsmul_add_comm'
theorem pow_boole : ∀ (P : Prop ) [inst : Decidable P a : M ), (a ^ if P then 1 else 0 = if P then a else 1 pow_boole ( P : Prop ) [ Decidable P ] ( a : M ) :
( a ^ if P then 1 else 0 ) = if P then a else 1 := by (a ^ if P then 1 else 0 = if P then a else 1 simp
#align pow_boole pow_boole : ∀ {M : Type u} [inst : Monoid M P : Prop ) [inst_1 : Decidable P a : M ),
(a ^ if P then 1 else 0 = if P then a else 1
@[ to_additive nsmul_left_comm ]
theorem pow_right_comm : ∀ (a : M ) (m n : ℕ ), (a ^ m ^ n = (a ^ n ^ m pow_right_comm ( a : M ) ( m n : ℕ ) : ( a ^ m ) ^ n = ( a ^ n ) ^ m := by
(a ^ m ^ n = (a ^ n ^ m rw [ (a ^ m ^ n = (a ^ n ^ m ← pow_mul : ∀ {M : Type ?u.24293} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m * n = (a ^ m ^ n , a ^ (m * n = (a ^ n ^ m (a ^ m ^ n = (a ^ n ^ m Nat.mul_comm : ∀ (n m : ℕ ), n * m = m * n , a ^ (n * m = (a ^ n ^ m (a ^ m ^ n = (a ^ n ^ m pow_mul : ∀ {M : Type ?u.24354} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m * n = (a ^ m ^ n (a ^ n ^ m = (a ^ n ^ m ]
#align pow_right_comm pow_right_comm : ∀ {M : Type u} [inst : Monoid M a : M ) (m n : ℕ ), (a ^ m ^ n = (a ^ n ^ m
#align nsmul_left_comm nsmul_left_comm
@[ to_additive nsmul_add_sub_nsmul : ∀ {M : Type u} [inst : AddMonoid M a : M ) {m n : ℕ }, m ≤ n m • a + (n - m • a = n • a ]
theorem pow_mul_pow_sub : ∀ {M : Type u} [inst : Monoid M a : M ) {m n : ℕ }, m ≤ n a ^ m * a ^ (n - m = a ^ n pow_mul_pow_sub ( a : M ) { m n : ℕ } ( h : m ≤ n ) : a ^ m * a ^ ( n - m ) = a ^ n := by
rw [ ← pow_add : ∀ {M : Type ?u.25936} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m + n = a ^ m * a ^ n , a ^ (m + (n - m = a ^ n Nat.add_comm : ∀ (n m : ℕ ), n + m = m + n , Nat.sub_add_cancel : ∀ {n m : ℕ }, m ≤ n n - m + m = n h ]
#align pow_mul_pow_sub pow_mul_pow_sub : ∀ {M : Type u} [inst : Monoid M a : M ) {m n : ℕ }, m ≤ n a ^ m * a ^ (n - m = a ^ n
#align nsmul_add_sub_nsmul nsmul_add_sub_nsmul : ∀ {M : Type u} [inst : AddMonoid M a : M ) {m n : ℕ }, m ≤ n m • a + (n - m • a = n • a
@[ to_additive sub_nsmul_nsmul_add : ∀ {M : Type u} [inst : AddMonoid M a : M ) {m n : ℕ }, m ≤ n (n - m • a + m • a = n • a ]
theorem pow_sub_mul_pow : ∀ {M : Type u} [inst : Monoid M a : M ) {m n : ℕ }, m ≤ n a ^ (n - m * a ^ m = a ^ n pow_sub_mul_pow ( a : M ) { m n : ℕ } ( h : m ≤ n ) : a ^ ( n - m ) * a ^ m = a ^ n := by
rw [ ← pow_add : ∀ {M : Type ?u.27570} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m + n = a ^ m * a ^ n , Nat.sub_add_cancel : ∀ {n m : ℕ }, m ≤ n n - m + m = n h ]
#align pow_sub_mul_pow pow_sub_mul_pow : ∀ {M : Type u} [inst : Monoid M a : M ) {m n : ℕ }, m ≤ n a ^ (n - m * a ^ m = a ^ n
#align sub_nsmul_nsmul_add sub_nsmul_nsmul_add : ∀ {M : Type u} [inst : AddMonoid M a : M ) {m n : ℕ }, m ≤ n (n - m • a + m • a = n • a
/-- If `x ^ n = 1`, then `x ^ m` is the same as `x ^ (m % n)` -/
@[ to_additive nsmul_eq_mod_nsmul : ∀ {M : Type u_1} [inst : AddMonoid M x : M } (m : ℕ ) {n : ℕ }, 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 : ℕ }, x ^ n = 1 x ^ m = x ^ (m % n pow_eq_pow_mod { M : Type _ : Type (?u.27699+1)} [ Monoid M ] { x : M } ( m : ℕ ) { n : ℕ } ( h : x ^ n = 1 ) :
x ^ m = x ^ ( m % n ) := by
have t : x ^ m = x ^ (n * (m / n + m % n t : x ^ m = x ^ ( n * ( m / n ) + m % n ) :=
congr_arg : ∀ {α : Sort ?u.31834} {β : Sort ?u.31833} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ ( fun a => x ^ a ) (( Nat.add_comm : ∀ (n m : ℕ ), n + m = m + n _ _ ). trans : ∀ {α : Sort ?u.31938} {a b c : α }, a = b b = c a = c trans ( Nat.mod_add_div : ∀ (m k : ℕ ), m % k + k * (m / k = m _ _ )). symm : ∀ {α : Sort ?u.31960} {a b : α }, a = b b = a symm
dsimp at t : x ^ m = x ^ (n * (m / n + m % n t
rw [ t : x ^ m = x ^ (n * (m / n + m % n t , pow_add : ∀ {M : Type ?u.32002} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m + n = a ^ m * a ^ n , x ^ (n * (m / n * x ^ (m % n = x ^ (m % n pow_mul : ∀ {M : Type ?u.32056} [inst : Monoid M a : M ) (m n : ℕ ), a ^ (m * n = (a ^ m ^ n , (x ^ n ^ (m / n * x ^ (m % n = x ^ (m % n h , one_pow : ∀ {M : Type ?u.32096} [inst : Monoid M n : ℕ ), 1 ^ n = 1 , one_mul x ^ (m % n = x ^ (m % n ]
#align pow_eq_pow_mod pow_eq_pow_mod : ∀ {M : Type u_1} [inst : Monoid M x : M } (m : ℕ ) {n : ℕ }, x ^ n = 1 x ^ m = x ^ (m % n
#align nsmul_eq_mod_nsmul nsmul_eq_mod_nsmul : ∀ {M : Type u_1} [inst : AddMonoid M x : M } (m : ℕ ) {n : ℕ }, n • x = 0 m • x = (m % n • x
@[ to_additive ]
theorem pow_mul_comm : ∀ (a : M ) (m n : ℕ ), a ^ m * a ^ n = a ^ n * a ^ m pow_mul_comm ( a : M ) ( m n : ℕ ) : a ^ m * a ^ n = a ^ n * a ^ m :=
Commute.pow_pow_self : ∀ {M : Type ?u.33835} [inst : Monoid M a : M ) (m n : ℕ ), Commute (a ^ m a ^ n a m n
#align pow_mul_comm pow_mul_comm : ∀ {M : Type u} [inst : Monoid M a : M ) (m n : ℕ ), a ^ m * a ^ n = a ^ n * a ^ m
#align nsmul_add_comm nsmul_add_comm
section Bit
set_option linter.deprecated false
@[ to_additive bit0_nsmul ]
theorem