AlgebraInLean.Chapter03.Sheet02

def AlgebraInLean.mpow {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) :

ℕ → M

We define this function inductively. mpow x n gives the element equal to multiplying the identity element n times by x.

Equations

AlgebraInLean.mpow x Nat.zero = AlgebraInLean.𝕖
AlgebraInLean.mpow x n.succ = AlgebraInLean.μ (AlgebraInLean.mpow x n) x

Instances For

source

@[simp]

theorem AlgebraInLean.mpow_zero {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) :

AlgebraInLean.mpow x 0 = AlgebraInLean.𝕖

source

@[simp]

theorem AlgebraInLean.mpow_succ_right {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (n : ℕ) :

AlgebraInLean.mpow x (n + 1) = AlgebraInLean.μ (AlgebraInLean.mpow x n) x

source

@[simp]

theorem AlgebraInLean.mpow_one {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) :

AlgebraInLean.mpow x 1 = x

x¹ = x

source

theorem AlgebraInLean.mpow_two {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) :

AlgebraInLean.mpow x 2 = AlgebraInLean.μ x x

x² = x * x

source

theorem AlgebraInLean.mpow_succ_left {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (n : ℕ) :

AlgebraInLean.mpow x (n + 1) = AlgebraInLean.μ x (AlgebraInLean.mpow x n)

x ^ (n + 1) = x * x ^ n

source

theorem AlgebraInLean.mpow_add {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (m : ℕ) (n : ℕ) :

AlgebraInLean.mpow x (m + n) = AlgebraInLean.μ (AlgebraInLean.mpow x m) (AlgebraInLean.mpow x n)

x ^ (m + n) = x ^ m * x ^ n

source

theorem AlgebraInLean.mpow_mul {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (m : ℕ) (n : ℕ) :

AlgebraInLean.mpow x (m * n) = AlgebraInLean.mpow (AlgebraInLean.mpow x m) n

x ^ (m * n) = (x ^ m) ^ n

source

@[simp]

theorem AlgebraInLean.mpow_id {M : Type u_1} [AlgebraInLean.Monoid M] (n : ℕ) :

AlgebraInLean.mpow AlgebraInLean.𝕖 n = AlgebraInLean.𝕖

e ^ n = e

source

theorem AlgebraInLean.mpow_comm_self {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (n : ℕ) :

AlgebraInLean.μ (AlgebraInLean.mpow x n) x = AlgebraInLean.μ x (AlgebraInLean.mpow x n)

source

theorem AlgebraInLean.mpow_comm_mpow {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (m : ℕ) (n : ℕ) :

AlgebraInLean.μ (AlgebraInLean.mpow x n) (AlgebraInLean.mpow x m) = AlgebraInLean.μ (AlgebraInLean.mpow x m) (AlgebraInLean.mpow x n)

source

def AlgebraInLean.gpow {G : Type u_1} [AlgebraInLean.Group G] (x : G) :

ℤ → G

Now, we define the power function for groups. Since groups have inverses, there becomes a natural notion of negative exponentiation. Notice that Int has two constructors of type Nat → Int.

Equations

AlgebraInLean.gpow x✝ x = match x with | Int.ofNat n => AlgebraInLean.mpow x✝ n | Int.negSucc n => AlgebraInLean.mpow (AlgebraInLean.ι x✝) (n + 1)

Instances For

source

theorem AlgebraInLean.gpow_ofNat {G : Type u_1} [AlgebraInLean.Group G] (x : G) (n : ℕ) :

AlgebraInLean.gpow x ↑n = AlgebraInLean.mpow x n

source

theorem AlgebraInLean.gpow_negSucc {G : Type u_1} [AlgebraInLean.Group G] (x : G) (n : ℕ) :

AlgebraInLean.gpow x (Int.negSucc n) = AlgebraInLean.mpow (AlgebraInLean.ι x) (n + 1)

source

theorem AlgebraInLean.inv_mpow {G : Type u_1} [AlgebraInLean.Group G] (x : G) (n : ℕ) :

AlgebraInLean.ι (AlgebraInLean.mpow x n) = AlgebraInLean.mpow (AlgebraInLean.ι x) n

source

@[simp]

theorem AlgebraInLean.gpow_zero {G : Type u_1} [AlgebraInLean.Group G] (x : G) :

AlgebraInLean.gpow x 0 = AlgebraInLean.𝕖

source

@[simp]

theorem AlgebraInLean.gpow_one {G : Type u_1} [AlgebraInLean.Group G] (x : G) :

AlgebraInLean.gpow x 1 = x

source

theorem AlgebraInLean.gpow_two {G : Type u_1} [AlgebraInLean.Group G] (x : G) :

AlgebraInLean.gpow x 2 = AlgebraInLean.μ x x

source

theorem AlgebraInLean.gpow_neg_mpow {G : Type u_1} [AlgebraInLean.Group G] (x : G) (n : ℕ) :

AlgebraInLean.gpow x (-↑n) = AlgebraInLean.ι (AlgebraInLean.mpow x n)

source

@[simp]

theorem AlgebraInLean.gpow_neg_one {G : Type u_1} [AlgebraInLean.Group G] (x : G) :

AlgebraInLean.gpow x (-1) = AlgebraInLean.ι x

source

@[simp]

theorem AlgebraInLean.gpow_succ {G : Type u_1} [AlgebraInLean.Group G] (x : G) (n : ℤ) :

AlgebraInLean.gpow x (n + 1) = AlgebraInLean.μ (AlgebraInLean.gpow x n) x

source

theorem AlgebraInLean.gpow_pred {G : Type u_1} [AlgebraInLean.Group G] (x : G) {n : ℤ} :

AlgebraInLean.μ (AlgebraInLean.gpow x n) (AlgebraInLean.ι x) = AlgebraInLean.gpow x (n - 1)

source

theorem AlgebraInLean.gpow_add {G : Type u_1} [AlgebraInLean.Group G] (x : G) {m : ℤ} {n : ℤ} :

AlgebraInLean.μ (AlgebraInLean.gpow x m) (AlgebraInLean.gpow x n) = AlgebraInLean.gpow x (m + n)

source

theorem AlgebraInLean.gpow_neg {G : Type u_1} [AlgebraInLean.Group G] (x : G) (n : ℤ) :

AlgebraInLean.gpow x (-n) = AlgebraInLean.ι (AlgebraInLean.gpow x n)

source

@[simp]

theorem AlgebraInLean.gpow_sub {G : Type u_1} [AlgebraInLean.Group G] (x : G) (m : ℤ) (n : ℤ) :

AlgebraInLean.μ (AlgebraInLean.gpow x m) (AlgebraInLean.ι (AlgebraInLean.gpow x n)) = AlgebraInLean.gpow x (m - n)

source

theorem AlgebraInLean.gpow_mul {G : Type u_1} [AlgebraInLean.Group G] (x : G) (m : ℤ) (n : ℤ) :

AlgebraInLean.gpow x (m * n) = AlgebraInLean.gpow (AlgebraInLean.gpow x m) n

source

theorem AlgebraInLean.gpow_closure {G : Type u_1} [AlgebraInLean.Group G] (x : G) {H : AlgebraInLean.Subgroup G} {n : ℤ} :

x ∈ H → AlgebraInLean.gpow x n ∈ H