mathlib docs: algebra.group

source

def monoid.pow {M : Type u} [has_mul M] [has_one M] :

M → ℕ → M

The power operation in a monoid. a^n = a*a*...*a n times.

Equations

monoid.pow a (n + 1) = a * monoid.pow a n
monoid.pow a 0 = 1

source

def nsmul {A : Type y} [has_add A] [has_zero A] :

ℕ → A → A

The scalar multiplication in an additive monoid. n •ℕ a = a+a+...+a n times.

Equations

n •ℕ a = monoid.pow a n

source

@[instance]

def monoid.has_pow {M : Type u} [monoid M] :

has_pow M ℕ

Equations

monoid.has_pow = {pow := monoid.pow (monoid.to_has_one M)}

source

@[simp]

theorem semiconj_by.pow_right {M : Type u} [monoid M] {a x y : M} (h : semiconj_by a x y) (n : ℕ) :

semiconj_by a (x ^ n) (y ^ n)

source

@[simp]

theorem commute.pow_right {M : Type u} [monoid M] {a b : M} (h : commute a b) (n : ℕ) :

commute a (b ^ n)

source

@[simp]

theorem commute.pow_left {M : Type u} [monoid M] {a b : M} (h : commute a b) (n : ℕ) :

commute (a ^ n) b

source

@[simp]

theorem commute.pow_pow {M : Type u} [monoid M] {a b : M} (h : commute a b) (m n : ℕ) :

commute (a ^ m) (b ^ n)

source

@[simp]

theorem commute.self_pow {M : Type u} [monoid M] (a : M) (n : ℕ) :

commute a (a ^ n)

source

@[simp]

theorem commute.pow_self {M : Type u} [monoid M] (a : M) (n : ℕ) :

commute (a ^ n) a

source

@[simp]

theorem commute.pow_pow_self {M : Type u} [monoid M] (a : M) (m n : ℕ) :

commute (a ^ m) (a ^ n)

source

@[simp]

theorem pow_zero {M : Type u} [monoid M] (a : M) :

a ^ 0 = 1

source

@[simp]

theorem zero_nsmul {A : Type y} [add_monoid A] (a : A) :

0 •ℕ a = 0

source

theorem pow_succ {M : Type u} [monoid M] (a : M) (n : ℕ) :

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

source

theorem succ_nsmul {A : Type y} [add_monoid A] (a : A) (n : ℕ) :

(n + 1) •ℕ a = a + n •ℕ a

source

@[simp]

theorem pow_one {M : Type u} [monoid M] (a : M) :

a ^ 1 = a

source

@[simp]

theorem one_nsmul {A : Type y} [add_monoid A] (a : A) :

1 •ℕ a = a

source

@[simp]

theorem pow_ite {M : Type u} [monoid M] (P : Prop) [decidable P] (a : M) (b c : ℕ) :

a ^ ite P b c = ite P (a ^ b) (a ^ c)

source

@[simp]

theorem ite_pow {M : Type u} [monoid M] (P : Prop) [decidable P] (a b : M) (c : ℕ) :

ite P a b ^ c = ite P (a ^ c) (b ^ c)

source

@[simp]

theorem pow_boole {M : Type u} [monoid M] (P : Prop) [decidable P] (a : M) :

a ^ ite P 1 0 = ite P a 1

source

theorem pow_mul_comm' {M : Type u} [monoid M] (a : M) (n : ℕ) :

a ^ n * a = a * a ^ n

source

theorem nsmul_add_comm' {A : Type y} [add_monoid A] (a : A) (n : ℕ) :

n •ℕ a + a = a + n •ℕ a

source

theorem pow_succ' {M : Type u} [monoid M] (a : M) (n : ℕ) :

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

source

theorem succ_nsmul' {A : Type y} [add_monoid A] (a : A) (n : ℕ) :

(n + 1) •ℕ a = n •ℕ a + a

source

theorem pow_two {M : Type u} [monoid M] (a : M) :

a ^ 2 = a * a

source

theorem two_nsmul {A : Type y} [add_monoid A] (a : A) :

2 •ℕ a = a + a

source

theorem pow_add {M : Type u} [monoid M] (a : M) (m n : ℕ) :

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

source

theorem add_nsmul {A : Type y} [add_monoid A] (a : A) (m n : ℕ) :

(m + n) •ℕ a = m •ℕ a + n •ℕ a

source

@[simp]

theorem one_pow {M : Type u} [monoid M] (n : ℕ) :

1 ^ n = 1

source

@[simp]

theorem nsmul_zero {A : Type y} [add_monoid A] (n : ℕ) :

n •ℕ 0 = 0

source

theorem pow_mul {M : Type u} [monoid M] (a : M) (m n : ℕ) :

a ^ (m * n) = (a ^ m) ^ n

source

theorem mul_nsmul' {A : Type y} [add_monoid A] (a : A) (m n : ℕ) :

m * n •ℕ a = n •ℕ (m •ℕ a)

source

theorem pow_mul' {M : Type u} [monoid M] (a : M) (m n : ℕ) :

a ^ (m * n) = (a ^ n) ^ m

source

theorem mul_nsmul {A : Type y} [add_monoid A] (a : A) (m n : ℕ) :

m * n •ℕ a = m •ℕ (n •ℕ a)

source

@[simp]

theorem nsmul_one {A : Type y} [add_monoid A] [has_one A] (n : ℕ) :

n •ℕ 1 = ↑n

source

theorem pow_bit0 {M : Type u} [monoid M] (a : M) (n : ℕ) :

a ^ bit0 n = a ^ n * a ^ n

source

theorem bit0_nsmul {A : Type y} [add_monoid A] (a : A) (n : ℕ) :

bit0 n •ℕ a = n •ℕ a + n •ℕ a

source

theorem pow_bit1 {M : Type u} [monoid M] (a : M) (n : ℕ) :

a ^ bit1 n = a ^ n * a ^ n * a

source

theorem bit1_nsmul {A : Type y} [add_monoid A] (a : A) (n : ℕ) :

bit1 n •ℕ a = n •ℕ a + n •ℕ a + a

source

theorem pow_mul_comm {M : Type u} [monoid M] (a : M) (m n : ℕ) :

a ^ m * a ^ n = a ^ n * a ^ m

source

theorem nsmul_add_comm {A : Type y} [add_monoid A] (a : A) (m n : ℕ) :

m •ℕ a + n •ℕ a = n •ℕ a + m •ℕ a

source

@[simp]

theorem list.prod_repeat {M : Type u} [monoid M] (a : M) (n : ℕ) :

(list.repeat a n).prod = a ^ n

source

@[simp]

theorem list.sum_repeat {A : Type y} [add_monoid A] (a : A) (n : ℕ) :

(list.repeat a n).sum = n •ℕ a

source

theorem monoid_hom.map_pow {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M →* N) (a : M) (n : ℕ) :

⇑f (a ^ n) = ⇑f a ^ n

source

theorem add_monoid_hom.map_nsmul {A : Type y} {B : Type z} [add_monoid A] [add_monoid B] (f : A →+ B) (a : A) (n : ℕ) :

⇑f (n •ℕ a) = n •ℕ ⇑f a

source

theorem is_monoid_hom.map_pow {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M → N) [is_monoid_hom f] (a : M) (n : ℕ) :

f (a ^ n) = f a ^ n

source

theorem is_add_monoid_hom.map_nsmul {A : Type y} {B : Type z} [add_monoid A] [add_monoid B] (f : A → B) [is_add_monoid_hom f] (a : A) (n : ℕ) :

f (n •ℕ a) = n •ℕ f a

source

@[simp]

theorem units.coe_pow {M : Type u} [monoid M] (u : units M) (n : ℕ) :

↑(u ^ n) = ↑u ^ n

source

theorem commute.mul_pow {M : Type u} [monoid M] {a b : M} (h : commute a b) (n : ℕ) :

(a * b) ^ n = a ^ n * b ^ n

source

theorem neg_pow {R : Type u₁} [ring R] (a : R) (n : ℕ) :

(-a) ^ n = (-1) ^ n * a ^ n

source

@[simp]

theorem nat.pow_eq_pow (p q : ℕ) :

p ^ q = p ^ q

source

theorem nat.nsmul_eq_mul (m n : ℕ) :

m •ℕ n = m * n

source

theorem mul_pow {M : Type u} [comm_monoid M] (a b : M) (n : ℕ) :

(a * b) ^ n = a ^ n * b ^ n

source

theorem nsmul_add {A : Type y} [add_comm_monoid A] (a b : A) (n : ℕ) :

n •ℕ (a + b) = n •ℕ a + n •ℕ b

source

@[instance]

def pow.is_monoid_hom {M : Type u} [comm_monoid M] (n : ℕ) :

is_monoid_hom (λ (_x : M), _x ^ n)

Equations

_ = _

source

@[instance]

def nsmul.is_add_monoid_hom {A : Type y} [add_comm_monoid A] (n : ℕ) :

is_add_monoid_hom (nsmul n)

Equations

_ = _

source

theorem dvd_pow {M : Type u} [comm_monoid M] {x y : M} {n : ℕ} :

x ∣ y → n ≠ 0 → x ∣ y ^ n

source

@[simp]

theorem inv_pow {G : Type w} [group G] (a : G) (n : ℕ) :

a⁻¹ ^ n = (a ^ n)⁻¹

source

@[simp]

theorem neg_nsmul {A : Type y} [add_group A] (a : A) (n : ℕ) :

n •ℕ -a = -(n •ℕ a)

source

theorem pow_sub {G : Type w} [group G] (a : G) {m n : ℕ} :

n ≤ m → a ^ (m - n) = a ^ m * (a ^ n)⁻¹

source

theorem nsmul_sub {A : Type y} [add_group A] (a : A) {m n : ℕ} :

n ≤ m → (m - n) •ℕ a = m •ℕ a - n •ℕ a

source

theorem pow_inv_comm {G : Type w} [group G] (a : G) (m n : ℕ) :

a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m

source

theorem nsmul_neg_comm {A : Type y} [add_group A] (a : A) (m n : ℕ) :

m •ℕ -a + n •ℕ a = n •ℕ a + m •ℕ -a

source

def gpow {G : Type w} [group G] :

G → ℤ → G

The power operation in a group. This extends monoid.pow to negative integers with the definition a^(-n) = (a^n)⁻¹.

Equations

gpow a -[1+ n] = (a ^ n.succ)⁻¹
gpow a (int.of_nat n) = a ^ n

source

def gsmul {A : Type y} [add_group A] :

ℤ → A → A

The scalar multiplication by integers on an additive group. This extends nsmul to negative integers with the definition (-n) •ℤ a = -(n •ℕ a).

Equations

n •ℤ a = gpow a n

source

@[instance]

def group.has_pow {G : Type w} [group G] :

has_pow G ℤ

Equations

group.has_pow = {pow := gpow _inst_1}

source

@[simp]

theorem gpow_coe_nat {G : Type w} [group G] (a : G) (n : ℕ) :

a ^ ↑n = a ^ n

source

@[simp]

theorem gsmul_coe_nat {A : Type y} [add_group A] (a : A) (n : ℕ) :

↑n •ℤ a = n •ℕ a

source

theorem gpow_of_nat {G : Type w} [group G] (a : G) (n : ℕ) :

a ^ int.of_nat n = a ^ n

source

theorem gsmul_of_nat {A : Type y} [add_group A] (a : A) (n : ℕ) :

int.of_nat n •ℤ a = n •ℕ a

source

@[simp]

theorem gpow_neg_succ_of_nat {G : Type w} [group G] (a : G) (n : ℕ) :

a ^ -[1+ n] = (a ^ n.succ)⁻¹

source

@[simp]

theorem gsmul_neg_succ_of_nat {A : Type y} [add_group A] (a : A) (n : ℕ) :

-[1+ n] •ℤ a = -(n.succ •ℕ a)

source

@[simp]

theorem gpow_zero {G : Type w} [group G] (a : G) :

a ^ 0 = 1

source

@[simp]

theorem zero_gsmul {A : Type y} [add_group A] (a : A) :

0 •ℤ a = 0

source

@[simp]

theorem gpow_one {G : Type w} [group G] (a : G) :

a ^ 1 = a

source

@[simp]

theorem one_gsmul {A : Type y} [add_group A] (a : A) :

1 •ℤ a = a

source

@[simp]

theorem one_gpow {G : Type w} [group G] (n : ℤ) :

1 ^ n = 1

source

@[simp]

theorem gsmul_zero {A : Type y} [add_group A] (n : ℤ) :

n •ℤ 0 = 0

source

@[simp]

theorem gpow_neg {G : Type w} [group G] (a : G) (n : ℤ) :

a ^ -n = (a ^ n)⁻¹

source

theorem mul_gpow_neg_one {G : Type w} [group G] (a b : G) :

(a * b) ^ -1 = b ^ -1 * a ^ -1

source

@[simp]

theorem neg_gsmul {A : Type y} [add_group A] (a : A) (n : ℤ) :

-n •ℤ a = -(n •ℤ a)

source

theorem gpow_neg_one {G : Type w} [group G] (x : G) :

x ^ -1 = x⁻¹

source

theorem neg_one_gsmul {A : Type y} [add_group A] (x : A) :

(-1) •ℤ x = -x

source

theorem gsmul_one {A : Type y} [add_group A] [has_one A] (n : ℤ) :

n •ℤ 1 = ↑n

source

theorem inv_gpow {G : Type w} [group G] (a : G) (n : ℤ) :

a⁻¹ ^ n = (a ^ n)⁻¹

source

theorem gsmul_neg {A : Type y} [add_group A] (a : A) (n : ℤ) :

n •ℤ -a = -(n •ℤ a)

source

theorem gpow_add_one {G : Type w} [group G] (a : G) (n : ℤ) :

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

source

theorem add_one_gsmul {A : Type y} [add_group A] (a : A) (i : ℤ) :

(i + 1) •ℤ a = i •ℤ a + a

source

theorem gpow_sub_one {G : Type w} [group G] (a : G) (n : ℤ) :

a ^ (n - 1) = a ^ n * a⁻¹

source

theorem gpow_add {G : Type w} [group G] (a : G) (m n : ℤ) :

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

source

theorem mul_self_gpow {G : Type w} [group G] (b : G) (m : ℤ) :

b * b ^ m = b ^ (m + 1)

source

theorem mul_gpow_self {G : Type w} [group G] (b : G) (m : ℤ) :

b ^ m * b = b ^ (m + 1)

source

theorem add_gsmul {A : Type y} [add_group A] (a : A) (i j : ℤ) :

(i + j) •ℤ a = i •ℤ a + j •ℤ a

source

theorem gpow_sub {G : Type w} [group G] (a : G) (m n : ℤ) :

a ^ (m - n) = a ^ m * (a ^ n)⁻¹

source

theorem sub_gsmul {A : Type y} [add_group A] (m n : ℤ) (a : A) :

(m - n) •ℤ a = m •ℤ a - n •ℤ a

source

theorem gpow_one_add {G : Type w} [group G] (a : G) (i : ℤ) :

a ^ (1 + i) = a * a ^ i

source

theorem one_add_gsmul {A : Type y} [add_group A] (a : A) (i : ℤ) :

(1 + i) •ℤ a = a + i •ℤ a

source

theorem gpow_mul_comm {G : Type w} [group G] (a : G) (i j : ℤ) :

a ^ i * a ^ j = a ^ j * a ^ i

source

theorem gsmul_add_comm {A : Type y} [add_group A] (a : A) (i j : ℤ) :

i •ℤ a + j •ℤ a = j •ℤ a + i •ℤ a

source

theorem gpow_mul {G : Type w} [group G] (a : G) (m n : ℤ) :

a ^ (m * n) = (a ^ m) ^ n

source

theorem gsmul_mul' {A : Type y} [add_group A] (a : A) (m n : ℤ) :

m * n •ℤ a = n •ℤ (m •ℤ a)

source

theorem gpow_mul' {G : Type w} [group G] (a : G) (m n : ℤ) :

a ^ (m * n) = (a ^ n) ^ m

source

theorem gsmul_mul {A : Type y} [add_group A] (a : A) (m n : ℤ) :

m * n •ℤ a = m •ℤ (n •ℤ a)

source

theorem gpow_bit0 {G : Type w} [group G] (a : G) (n : ℤ) :

a ^ bit0 n = a ^ n * a ^ n

source

theorem bit0_gsmul {A : Type y} [add_group A] (a : A) (n : ℤ) :

bit0 n •ℤ a = n •ℤ a + n •ℤ a

source

theorem gpow_bit1 {G : Type w} [group G] (a : G) (n : ℤ) :

a ^ bit1 n = a ^ n * a ^ n * a

source

theorem bit1_gsmul {A : Type y} [add_group A] (a : A) (n : ℤ) :

bit1 n •ℤ a = n •ℤ a + n •ℤ a + a

source

theorem monoid_hom.map_gpow {G : Type w} {H : Type x} [group G] [group H] (f : G →* H) (a : G) (n : ℤ) :

⇑f (a ^ n) = ⇑f a ^ n

source

theorem add_monoid_hom.map_gsmul {A : Type y} {B : Type z} [add_group A] [add_group B] (f : A →+ B) (a : A) (n : ℤ) :

⇑f (n •ℤ a) = n •ℤ ⇑f a

source

@[simp]

theorem units.coe_gpow {G : Type w} [group G] (u : units G) (n : ℤ) :

↑(u ^ n) = ↑u ^ n

source

theorem commute.mul_gpow {G : Type w} [group G] {a b : G} (h : commute a b) (n : ℤ) :

(a * b) ^ n = a ^ n * b ^ n

source

theorem mul_gpow {G : Type w} [comm_group G] (a b : G) (n : ℤ) :

(a * b) ^ n = a ^ n * b ^ n

source

theorem gsmul_add {A : Type y} [add_comm_group A] (a b : A) (n : ℤ) :

n •ℤ (a + b) = n •ℤ a + n •ℤ b

source

theorem gsmul_sub {A : Type y} [add_comm_group A] (a b : A) (n : ℤ) :

n •ℤ (a - b) = n •ℤ a - n •ℤ b

source

@[instance]

def gpow.is_group_hom {G : Type w} [comm_group G] (n : ℤ) :

is_group_hom (λ (_x : G), _x ^ n)

Equations

_ = is_group_hom.mk

source

@[instance]

def gsmul.is_add_group_hom {A : Type y} [add_comm_group A] (n : ℤ) :

is_add_group_hom (gsmul n)

Equations

_ = is_add_group_hom.mk

source

@[simp]

theorem with_bot.coe_nsmul {A : Type y} [add_monoid A] (a : A) (n : ℕ) :

↑(n •ℕ a) = n •ℕ ↑a

source

theorem nsmul_eq_mul' {R : Type u₁} [semiring R] (a : R) (n : ℕ) :

n •ℕ a = a * ↑n

source

@[simp]

theorem nsmul_eq_mul {R : Type u₁} [semiring R] (n : ℕ) (a : R) :

n •ℕ a = ↑n * a

source

theorem mul_nsmul_left {R : Type u₁} [semiring R] (a b : R) (n : ℕ) :

n •ℕ (a * b) = a * (n •ℕ b)

source

theorem mul_nsmul_assoc {R : Type u₁} [semiring R] (a b : R) (n : ℕ) :

n •ℕ (a * b) = n •ℕ a * b

source

theorem zero_pow {R : Type u₁} [monoid_with_zero R] {n : ℕ} :

0 < n → 0 ^ n = 0

source

@[simp]

theorem nat.cast_pow {R : Type u₁} [semiring R] (n m : ℕ) :

↑(n ^ m) = ↑n ^ m

source

@[simp]

theorem int.coe_nat_pow (n m : ℕ) :

↑(n ^ m) = ↑n ^ m

source

theorem int.nat_abs_pow (n : ℤ) (k : ℕ) :

(n ^ k).nat_abs = n.nat_abs ^ k

source

@[simp]

theorem ring_hom.map_pow {R : Type u₁} {S : Type u₂} [semiring R] [semiring S] (f : R →+* S) (a : R) (n : ℕ) :

⇑f (a ^ n) = ⇑f a ^ n

source

theorem neg_one_pow_eq_or {R : Type u₁} [ring R] (n : ℕ) :

(-1) ^ n = 1 ∨ (-1) ^ n = -1

source

theorem pow_dvd_pow {R : Type u₁} [monoid R] (a : R) {m n : ℕ} :

m ≤ n → a ^ m ∣ a ^ n

source

theorem pow_dvd_pow_of_dvd {R : Type u₁} [comm_monoid R] {a b : R} (h : a ∣ b) (n : ℕ) :

a ^ n ∣ b ^ n

source

theorem pow_two_sub_pow_two {R : Type u_1} [comm_ring R] (a b : R) :

a ^ 2 - b ^ 2 = (a + b) * (a - b)

source

theorem eq_or_eq_neg_of_pow_two_eq_pow_two {R : Type u₁} [integral_domain R] (a b : R) :

a ^ 2 = b ^ 2 → a = b ∨ a = -b

source

theorem bit0_mul {R : Type u₁} [ring R] {n r : R} :

bit0 n * r = 2 •ℤ (n * r)

source

theorem mul_bit0 {R : Type u₁} [ring R] {n r : R} :

r * bit0 n = 2 •ℤ (r * n)

source

theorem bit1_mul {R : Type u₁} [ring R] {n r : R} :

bit1 n * r = 2 •ℤ (n * r) + r

source

theorem mul_bit1 {R : Type u₁} [ring R] {n r : R} :

r * bit1 n = 2 •ℤ (r * n) + r

source

@[simp]

theorem gsmul_eq_mul {R : Type u₁} [ring R] (a : R) (n : ℤ) :

n •ℤ a = ↑n * a

source

theorem gsmul_eq_mul' {R : Type u₁} [ring R] (a : R) (n : ℤ) :

n •ℤ a = a * ↑n

source

theorem mul_gsmul_left {R : Type u₁} [ring R] (a b : R) (n : ℤ) :

n •ℤ (a * b) = a * (n •ℤ b)

source

theorem mul_gsmul_assoc {R : Type u₁} [ring R] (a b : R) (n : ℤ) :

n •ℤ (a * b) = n •ℤ a * b

source

@[simp]

theorem gsmul_int_int (a b : ℤ) :

a •ℤ b = a * b

source

theorem gsmul_int_one (n : ℤ) :

n •ℤ 1 = n

source

@[simp]

theorem int.cast_pow {R : Type u₁} [ring R] (n : ℤ) (m : ℕ) :

↑(n ^ m) = ↑n ^ m

source

theorem neg_one_pow_eq_pow_mod_two {R : Type u₁} [ring R] {n : ℕ} :

(-1) ^ n = (-1) ^ (n % 2)

source

theorem sq_sub_sq {R : Type u₁} [comm_ring R] (a b : R) :

a ^ 2 - b ^ 2 = (a + b) * (a - b)

source

theorem pow_eq_zero {R : Type u₁} [monoid_with_zero R] [no_zero_divisors R] {x : R} {n : ℕ} :

x ^ n = 0 → x = 0

source

theorem pow_ne_zero {R : Type u₁} [monoid_with_zero R] [no_zero_divisors R] {a : R} (n : ℕ) :

a ≠ 0 → a ^ n ≠ 0

source

theorem nsmul_nonneg {R : Type u₁} [ordered_add_comm_monoid R] {a : R} (H : 0 ≤ a) (n : ℕ) :

0 ≤ n •ℕ a

source

theorem pow_abs {R : Type u₁} [decidable_linear_ordered_comm_ring R] (a : R) (n : ℕ) :

abs a ^ n = abs (a ^ n)

source

theorem abs_neg_one_pow {R : Type u₁} [decidable_linear_ordered_comm_ring R] (n : ℕ) :

abs ((-1) ^ n) = 1

source

theorem nsmul_le_nsmul {A : Type y} [ordered_add_comm_monoid A] {a : A} {n m : ℕ} :

0 ≤ a → n ≤ m → n •ℕ a ≤ m •ℕ a

source

theorem nsmul_le_nsmul_of_le_right {A : Type y} [ordered_add_comm_monoid A] {a b : A} (hab : a ≤ b) (i : ℕ) :

i •ℕ a ≤ i •ℕ b

source

theorem canonically_ordered_semiring.pow_pos {R : Type u₁} [canonically_ordered_comm_semiring R] {a : R} (H : 0 < a) (n : ℕ) :

0 < a ^ n

source

theorem canonically_ordered_semiring.pow_le_pow_of_le_left {R : Type u₁} [canonically_ordered_comm_semiring R] {a b : R} (hab : a ≤ b) (i : ℕ) :

a ^ i ≤ b ^ i

source

theorem canonically_ordered_semiring.one_le_pow_of_one_le {R : Type u₁} [canonically_ordered_comm_semiring R] {a : R} (H : 1 ≤ a) (n : ℕ) :

1 ≤ a ^ n

source

theorem canonically_ordered_semiring.pow_le_one {R : Type u₁} [canonically_ordered_comm_semiring R] {a : R} (H : a ≤ 1) (n : ℕ) :

a ^ n ≤ 1

source

theorem pow_pos {R : Type u₁} [linear_ordered_semiring R] {a : R} (H : 0 < a) (n : ℕ) :

0 < a ^ n

source

theorem pow_nonneg {R : Type u₁} [linear_ordered_semiring R] {a : R} (H : 0 ≤ a) (n : ℕ) :

0 ≤ a ^ n

source

theorem pow_lt_pow_of_lt_left {R : Type u₁} [linear_ordered_semiring R] {x y : R} {n : ℕ} :

x < y → 0 ≤ x → 0 < n → x ^ n < y ^ n

source

theorem pow_left_inj {R : Type u₁} [linear_ordered_semiring R] {x y : R} {n : ℕ} :

0 ≤ x → 0 ≤ y → 0 < n → x ^ n = y ^ n → x = y

source

theorem one_le_pow_of_one_le {R : Type u₁} [linear_ordered_semiring R] {a : R} (H : 1 ≤ a) (n : ℕ) :

1 ≤ a ^ n

source

theorem one_add_mul_le_pow' {R : Type u₁} [linear_ordered_semiring R] {a : R} (Hsqr : 0 ≤ a * a) (H : 0 ≤ 1 + a) (n : ℕ) :

1 + n •ℕ a ≤ (1 + a) ^ n

Bernoulli's inequality. This version works for semirings but requires an additional hypothesis 0 ≤ a * a.

source

theorem pow_le_pow {R : Type u₁} [linear_ordered_semiring R] {a : R} {n m : ℕ} :

1 ≤ a → n ≤ m → a ^ n ≤ a ^ m

source

theorem pow_lt_pow {R : Type u₁} [linear_ordered_semiring R] {a : R} {n m : ℕ} :

1 < a → n < m → a ^ n < a ^ m

source

theorem pow_le_pow_of_le_left {R : Type u₁} [linear_ordered_semiring R] {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) (i : ℕ) :

a ^ i ≤ b ^ i

source

theorem lt_of_pow_lt_pow {R : Type u₁} [linear_ordered_semiring R] {a b : R} (n : ℕ) :

0 ≤ b → a ^ n < b ^ n → a < b

source

theorem pow_lt_pow_of_lt_one {R : Type u₁} [linear_ordered_semiring R] {a : R} (h : 0 < a) (ha : a < 1) {i j : ℕ} :

i < j → a ^ j < a ^ i

source

theorem pow_le_pow_of_le_one {R : Type u₁} [linear_ordered_semiring R] {a : R} (h : 0 ≤ a) (ha : a ≤ 1) {i j : ℕ} :

i ≤ j → a ^ j ≤ a ^ i

source

theorem pow_le_one {R : Type u₁} [linear_ordered_semiring R] {x : R} (n : ℕ) :

0 ≤ x → x ≤ 1 → x ^ n ≤ 1

source

theorem pow_two_nonneg {R : Type u₁} [linear_ordered_ring R] (a : R) :

0 ≤ a ^ 2

source

theorem pow_two_pos_of_ne_zero {R : Type u₁} [linear_ordered_ring R] (a : R) :

a ≠ 0 → 0 < a ^ 2

source

theorem one_add_mul_le_pow {R : Type u₁} [linear_ordered_ring R] {a : R} (H : -2 ≤ a) (n : ℕ) :

1 + n •ℕ a ≤ (1 + a) ^ n

Bernoulli's inequality for n : ℕ, -2 ≤ a.

source

theorem one_add_sub_mul_le_pow {R : Type u₁} [linear_ordered_ring R] {a : R} (H : -1 ≤ a) (n : ℕ) :

1 + n •ℕ (a - 1) ≤ a ^ n

Bernoulli's inequality reformulated to estimate a^n.

source

theorem int.units_pow_two (u : units ℤ) :

u ^ 2 = 1

source

theorem int.units_pow_eq_pow_mod_two (u : units ℤ) (n : ℕ) :

u ^ n = u ^ (n % 2)

source

@[simp]

theorem int.nat_abs_pow_two (x : ℤ) :

↑(x.nat_abs) ^ 2 = x ^ 2

source

@[simp]

theorem neg_square {α : Type u_1} [ring α] (z : α) :

(-z) ^ 2 = z ^ 2

source

theorem of_add_nsmul {A : Type y} [add_monoid A] (x : A) (n : ℕ) :

multiplicative.of_add (n •ℕ x) = multiplicative.of_add x ^ n

source

theorem of_add_gsmul {A : Type y} [add_group A] (x : A) (n : ℤ) :

multiplicative.of_add (n •ℤ x) = multiplicative.of_add x ^ n

source

def powers_hom (M : Type u) [monoid M] :

M ≃ (multiplicative ℕ →* M)

Monoid homomorphisms from multiplicative ℕ are defined by the image of multiplicative.of_add 1.

Equations

powers_hom M = {to_fun := λ (x : M), {to_fun := λ (n : multiplicative ℕ), x ^ n.to_add, map_one' := _, map_mul' := _}, inv_fun := λ (f : multiplicative ℕ →* M), ⇑f (multiplicative.of_add 1), left_inv := _, right_inv := _}

source

def gpowers_hom (G : Type w) [group G] :

G ≃ (multiplicative ℤ →* G)

Monoid homomorphisms from multiplicative ℤ are defined by the image of multiplicative.of_add 1.

Equations

gpowers_hom G = {to_fun := λ (x : G), {to_fun := λ (n : multiplicative ℤ), x ^ n.to_add, map_one' := _, map_mul' := _}, inv_fun := λ (f : multiplicative ℤ →* G), ⇑f (multiplicative.of_add 1), left_inv := _, right_inv := _}

source

def multiples_hom (A : Type y) [add_monoid A] :

A ≃ (ℕ →+ A)

Additive homomorphisms from ℕ are defined by the image of 1.

Equations

multiples_hom A = {to_fun := λ (x : A), {to_fun := λ (n : ℕ), n •ℕ x, map_zero' := _, map_add' := _}, inv_fun := λ (f : ℕ →+ A), ⇑f 1, left_inv := _, right_inv := _}

source

def gmultiples_hom (A : Type y) [add_group A] :

A ≃ (ℤ →+ A)

Additive homomorphisms from ℤ are defined by the image of 1.

Equations

gmultiples_hom A = {to_fun := λ (x : A), {to_fun := λ (n : ℤ), n •ℤ x, map_zero' := _, map_add' := _}, inv_fun := λ (f : ℤ →+ A), ⇑f 1, left_inv := _, right_inv := _}

source

@[simp]

theorem powers_hom_apply {M : Type u} [monoid M] (x : M) (n : multiplicative ℕ) :

⇑(⇑(powers_hom M) x) n = x ^ n.to_add

source

@[simp]

theorem powers_hom_symm_apply {M : Type u} [monoid M] (f : multiplicative ℕ →* M) :

⇑((powers_hom M).symm) f = ⇑f (multiplicative.of_add 1)

source

theorem mnat_monoid_hom_eq {M : Type u} [monoid M] (f : multiplicative ℕ →* M) (n : multiplicative ℕ) :

⇑f n = ⇑f (multiplicative.of_add 1) ^ n.to_add

source

theorem mnat_monoid_hom_ext {M : Type u} [monoid M] ⦃f g : multiplicative ℕ →* M⦄ :

⇑f (multiplicative.of_add 1) = ⇑g (multiplicative.of_add 1) → f = g

source

@[simp]

theorem semiconj_by.cast_nat_mul_right {R : Type u₁} [semiring R] {a x y : R} (h : semiconj_by a x y) (n : ℕ) :

semiconj_by a (↑n * x) (↑n * y)

source

@[simp]

theorem semiconj_by.cast_nat_mul_left {R : Type u₁} [semiring R] {a x y : R} (h : semiconj_by a x y) (n : ℕ) :

semiconj_by (↑n * a) x y

source

@[simp]

theorem semiconj_by.cast_nat_mul_cast_nat_mul {R : Type u₁} [semiring R] {a x y : R} (h : semiconj_by a x y) (m n : ℕ) :

semiconj_by (↑m * a) (↑n * x) (↑n * y)

source

@[simp]

theorem semiconj_by.units_gpow_right {M : Type u} [monoid M] {a : M} {x y : units M} (h : semiconj_by a ↑x ↑y) (m : ℤ) :

semiconj_by a ↑(x ^ m) ↑(y ^ m)

source

@[simp]

theorem semiconj_by.gpow_right {G : Type w} [group G] {a x y : G} (h : semiconj_by a x y) (m : ℤ) :

semiconj_by a (x ^ m) (y ^ m)

source

@[simp]

theorem semiconj_by.cast_int_mul_right {R : Type u₁} [ring R] {a x y : R} (h : semiconj_by a x y) (m : ℤ) :

semiconj_by a (↑m * x) (↑m * y)

source

@[simp]

theorem semiconj_by.cast_int_mul_left {R : Type u₁} [ring R] {a x y : R} (h : semiconj_by a x y) (m : ℤ) :

semiconj_by (↑m * a) x y

source

@[simp]

theorem semiconj_by.cast_int_mul_cast_int_mul {R : Type u₁} [ring R] {a x y : R} (h : semiconj_by a x y) (m n : ℤ) :

semiconj_by (↑m * a) (↑n * x) (↑n * y)

source

@[simp]

theorem commute.cast_nat_mul_right {R : Type u₁} [semiring R] {a b : R} (h : commute a b) (n : ℕ) :

commute a (↑n * b)

source

@[simp]

theorem commute.cast_nat_mul_left {R : Type u₁} [semiring R] {a b : R} (h : commute a b) (n : ℕ) :

commute (↑n * a) b

source

@[simp]

theorem commute.cast_nat_mul_cast_nat_mul {R : Type u₁} [semiring R] {a b : R} (h : commute a b) (m n : ℕ) :

commute (↑m * a) (↑n * b)

source

@[simp]

theorem commute.self_cast_nat_mul {R : Type u₁} [semiring R] {a : R} (n : ℕ) :

commute a (↑n * a)

source

@[simp]

theorem commute.cast_nat_mul_self {R : Type u₁} [semiring R] {a : R} (n : ℕ) :

commute (↑n * a) a

source

@[simp]

theorem commute.self_cast_nat_mul_cast_nat_mul {R : Type u₁} [semiring R] {a : R} (m n : ℕ) :

commute (↑m * a) (↑n * a)

source

@[simp]

theorem commute.units_gpow_right {M : Type u} [monoid M] {a : M} {u : units M} (h : commute a ↑u) (m : ℤ) :

commute a ↑(u ^ m)

source

@[simp]

theorem commute.units_gpow_left {M : Type u} [monoid M] {u : units M} {a : M} (h : commute ↑u a) (m : ℤ) :

commute ↑(u ^ m) a

source

@[simp]

theorem commute.gpow_right {G : Type w} [group G] {a b : G} (h : commute a b) (m : ℤ) :

commute a (b ^ m)

source

@[simp]

theorem commute.gpow_left {G : Type w} [group G] {a b : G} (h : commute a b) (m : ℤ) :

commute (a ^ m) b

source

theorem commute.gpow_gpow {G : Type w} [group G] {a b : G} (h : commute a b) (m n : ℤ) :

commute (a ^ m) (b ^ n)

source

@[simp]

theorem commute.self_gpow {G : Type w} [group G] (a : G) (n : ℕ) :

commute a (a ^ n)

source

@[simp]

theorem commute.gpow_self {G : Type w} [group G] (a : G) (n : ℕ) :

commute (a ^ n) a

source

@[simp]

theorem commute.gpow_gpow_self {G : Type w} [group G] (a : G) (m n : ℕ) :

commute (a ^ m) (a ^ n)

source

@[simp]

theorem commute.cast_int_mul_right {R : Type u₁} [ring R] {a b : R} (h : commute a b) (m : ℤ) :

commute a (↑m * b)

source

@[simp]

theorem commute.cast_int_mul_left {R : Type u₁} [ring R] {a b : R} (h : commute a b) (m : ℤ) :

commute (↑m * a) b

source

theorem commute.cast_int_mul_cast_int_mul {R : Type u₁} [ring R] {a b : R} (h : commute a b) (m n : ℤ) :

commute (↑m * a) (↑n * b)

source

@[simp]

theorem commute.self_cast_int_mul {R : Type u₁} [ring R] (a : R) (n : ℤ) :

commute a (↑n * a)

source

@[simp]

theorem commute.cast_int_mul_self {R : Type u₁} [ring R] (a : R) (n : ℤ) :

commute (↑n * a) a

source

theorem commute.self_cast_int_mul_cast_int_mul {R : Type u₁} [ring R] (a : R) (m n : ℤ) :

commute (↑m * a) (↑n * a)

source

@[simp]

theorem nat.to_add_pow (a : multiplicative ℕ) (b : ℕ) :

(a ^ b).to_add = a.to_add * b

source

@[simp]

theorem nat.of_add_mul (a b : ℕ) :

multiplicative.of_add (a * b) = multiplicative.of_add a ^ b

source

@[simp]

theorem int.to_add_pow (a : multiplicative ℤ) (b : ℕ) :

(a ^ b).to_add = a.to_add * ↑b

source

@[simp]

theorem int.to_add_gpow (a : multiplicative ℤ) (b : ℤ) :

(a ^ b).to_add = a.to_add * b

source

@[simp]

theorem int.of_add_mul (a b : ℤ) :

multiplicative.of_add (a * b) = multiplicative.of_add a ^ b

source

theorem units.conj_pow {M : Type u} [monoid M] (u : units M) (x : M) (n : ℕ) :

(↑u * x * ↑u⁻¹) ^ n = ↑u * x ^ n * ↑u⁻¹

source

theorem units.conj_pow' {M : Type u} [monoid M] (u : units M) (x : M) (n : ℕ) :

(↑u⁻¹ * x * ↑u) ^ n = ↑u⁻¹ * x ^ n * ↑u

source

@[simp]

theorem units.op_pow {M : Type u} [monoid M] (x : M) (n : ℕ) :

opposite.op (x ^ n) = opposite.op x ^ n

Moving to the opposite monoid commutes with taking powers.

source

@[simp]

theorem units.unop_pow {M : Type u} [monoid M] (x : Mᵒᵖ) (n : ℕ) :

opposite.unop (x ^ n) = opposite.unop x ^ n

mathlib documentation

algebra.group_power

Power operations on monoids and groups

Notation

Implementation details

Commutativity

(Additive) monoid

Commutative (additive) monoid

Commutativity (again)

General documentation

Additional documentation

Library

mathlib documentation

algebra.​group_power

Power operations on monoids and groups

Notation

Implementation details

Commutativity

(Additive) monoid

Commutative (additive) monoid

Commutativity (again)

General documentation

Additional documentation

Library

algebra.group_power