mathlib3 documentation

algebra.group_power.lemmas

Lemmas about power operations on monoids and groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains lemmas about monoid.pow, group.pow, nsmul, zsmul which require additional imports besides those available in algebra.group_power.basic.

(Additive) monoid #

source
@[simp]
theorem nsmul_one {A : Type y} [add_monoid_with_one A] (n : ℕ) :
n • 1 = ↑n
source
@[protected, instance]
def invertible_pow {M : Type u} [monoid M] (m : M) [invertible m] (n : ℕ) :
invertible (m ^ n)
Equations
source
theorem inv_of_pow {M : Type u} [monoid M] (m : M) [invertible m] (n : ℕ) [invertible (m ^ n)] :
⅟ (m ^ n) = ⅟ m ^ n
source
theorem is_add_unit.nsmul {M : Type u} [add_monoid M] {m : M} (n : ℕ) :
is_add_unit m → is_add_unit (n • m)
source
theorem is_unit.pow {M : Type u} [monoid M] {m : M} (n : ℕ) :
is_unit m → is_unit (m ^ n)
source
def add_units.of_nsmul {M : Type u} [add_monoid M] (u : add_units M) (x : M) {n : ℕ} (hn : n ≠ 0) (hu : n • x = ↑u) :
add_units M

If a natural multiple of x is an additive unit, then x is an additive unit.

Equations
source
def units.of_pow {M : Type u} [monoid M] (u : Mˣ) (x : M) {n : ℕ} (hn : n ≠ 0) (hu : x ^ n = ↑u) :
Mˣ

If a natural power of x is a unit, then x is a unit.

Equations
source
@[simp]
theorem is_add_unit_nsmul_iff {M : Type u} [add_monoid M] {a : M} {n : ℕ} (hn : n ≠ 0) :
is_add_unit (n • a) ↔ is_add_unit a
source
@[simp]
theorem is_unit_pow_iff {M : Type u} [monoid M] {a : M} {n : ℕ} (hn : n ≠ 0) :
is_unit (a ^ n) ↔ is_unit a
source
theorem is_add_unit_nsmul_succ_iff {M : Type u} [add_monoid M] {m : M} {n : ℕ} :
is_add_unit ((n + 1) • m) ↔ is_add_unit m
source
theorem is_unit_pow_succ_iff {M : Type u} [monoid M] {m : M} {n : ℕ} :
is_unit (m ^ (n + 1)) ↔ is_unit m
source
@[simp]
theorem units.coe_inv_of_pow_eq_one {M : Type u} [monoid M] (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) :
↑(units.of_pow_eq_one x n hx hn)⁻¹ = x ^ (n - 1)
source
def add_units.of_nsmul_eq_zero {M : Type u} [add_monoid M] (x : M) (n : ℕ) (hx : n • x = 0) (hn : n ≠ 0) :
add_units M

If n • x = 0, n ≠ 0, then x is an additive unit.

Equations
source
@[simp]
theorem units.coe_of_pow_eq_one {M : Type u} [monoid M] (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) :
↑(units.of_pow_eq_one x n hx hn) = x
source
@[simp]
theorem add_units.coe_neg_of_nsmul_eq_zero {M : Type u} [add_monoid M] (x : M) (n : ℕ) (hx : n • x = 0) (hn : n ≠ 0) :
↑-add_units.of_nsmul_eq_zero x n hx hn = (n - 1) • x
source
def units.of_pow_eq_one {M : Type u} [monoid M] (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) :
Mˣ

If x ^ n = 1, n ≠ 0, then x is a unit.

Equations
source
@[simp]
theorem add_units.coe_of_nsmul_eq_zero {M : Type u} [add_monoid M] (x : M) (n : ℕ) (hx : n • x = 0) (hn : n ≠ 0) :
↑(add_units.of_nsmul_eq_zero x n hx hn) = x
source
@[simp]
theorem units.pow_of_pow_eq_one {M : Type u} [monoid M] {x : M} {n : ℕ} (hx : x ^ n = 1) (hn : n ≠ 0) :
units.of_pow_eq_one x n hx hn ^ n = 1
source
@[simp]
theorem add_units.nsmul_of_nsmul_eq_zero {M : Type u} [add_monoid M] {x : M} {n : ℕ} (hx : n • x = 0) (hn : n ≠ 0) :
n • add_units.of_nsmul_eq_zero x n hx hn = 0
source
theorem is_add_unit_of_nsmul_eq_zero {M : Type u} [add_monoid M] {x : M} {n : ℕ} (hx : n • x = 0) (hn : n ≠ 0) :
is_add_unit x
source
theorem is_unit_of_pow_eq_one {M : Type u} [monoid M] {x : M} {n : ℕ} (hx : x ^ n = 1) (hn : n ≠ 0) :
is_unit x
source
def invertible_of_pow_eq_one {M : Type u} [monoid M] (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) :
invertible x

If x ^ n = 1 then x has an inverse, x^(n - 1).

Equations
source
theorem smul_pow {M : Type u} {N : Type v} [monoid M] [monoid N] [mul_action M N] [is_scalar_tower M N N] [smul_comm_class M N N] (k : M) (x : N) (p : ℕ) :
(k • x) ^ p = k ^ p • x ^ p
source
@[simp]
theorem smul_pow' {M : Type u} {N : Type v} [monoid M] [monoid N] [mul_distrib_mul_action M N] (x : M) (m : N) (n : ℕ) :
x • m ^ n = (x • m) ^ n
source
theorem zsmul_one {A : Type y} [add_group_with_one A] (n : ℤ) :
n • 1 = ↑n
source
theorem mul_zsmul' {α : Type u_1} [subtraction_monoid α] (a : α) (m n : ℤ) :
(m * n) • a = n • m • a
source
theorem zpow_mul {α : Type u_1} [division_monoid α] (a : α) (m n : ℤ) :
a ^ (m * n) = (a ^ m) ^ n
source
theorem zpow_mul' {α : Type u_1} [division_monoid α] (a : α) (m n : ℤ) :
a ^ (m * n) = (a ^ n) ^ m
source
theorem mul_zsmul {α : Type u_1} [subtraction_monoid α] (a : α) (m n : ℤ) :
(m * n) • a = m • n • a
source
theorem bit0_zsmul {α : Type u_1} [subtraction_monoid α] (a : α) (n : ℤ) :
bit0 n • a = n • a + n • a
source
theorem zpow_bit0 {α : Type u_1} [division_monoid α] (a : α) (n : ℤ) :
a ^ bit0 n = a ^ n * a ^ n
source
theorem zpow_bit0' {α : Type u_1} [division_monoid α] (a : α) (n : ℤ) :
a ^ bit0 n = (a * a) ^ n
source
theorem bit0_zsmul' {α : Type u_1} [subtraction_monoid α] (a : α) (n : ℤ) :
bit0 n • a = n • (a + a)
source
@[simp]
theorem zpow_bit0_neg {α : Type u_1} [division_monoid α] [has_distrib_neg α] (x : α) (n : ℤ) :
(-x) ^ bit0 n = x ^ bit0 n
source
theorem zpow_add_one {G : Type w} [group G] (a : G) (n : ℤ) :
a ^ (n + 1) = a ^ n * a
source
theorem add_one_zsmul {G : Type w} [add_group G] (a : G) (n : ℤ) :
(n + 1) • a = n • a + a
source
theorem sub_one_zsmul {G : Type w} [add_group G] (a : G) (n : ℤ) :
(n - 1) • a = n • a + -a
source
theorem zpow_sub_one {G : Type w} [group G] (a : G) (n : ℤ) :
a ^ (n - 1) = a ^ n * a⁻¹
source
theorem zpow_add {G : Type w} [group G] (a : G) (m n : ℤ) :
a ^ (m + n) = a ^ m * a ^ n
source
theorem add_zsmul {G : Type w} [add_group G] (a : G) (m n : ℤ) :
(m + n) • a = m • a + n • a
source
theorem mul_self_zpow {G : Type w} [group G] (b : G) (m : ℤ) :
b * b ^ m = b ^ (m + 1)
source
theorem add_zsmul_self {G : Type w} [add_group G] (b : G) (m : ℤ) :
b + m • b = (m + 1) • b
source
theorem add_self_zsmul {G : Type w} [add_group G] (b : G) (m : ℤ) :
m • b + b = (m + 1) • b
source
theorem mul_zpow_self {G : Type w} [group G] (b : G) (m : ℤ) :
b ^ m * b = b ^ (m + 1)
source
theorem sub_zsmul {G : Type w} [add_group G] (a : G) (m n : ℤ) :
(m - n) • a = m • a + -(n • a)
source
theorem zpow_sub {G : Type w} [group G] (a : G) (m n : ℤ) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
source
theorem one_add_zsmul {G : Type w} [add_group G] (a : G) (i : ℤ) :
(1 + i) • a = a + i • a
source
theorem zpow_one_add {G : Type w} [group G] (a : G) (i : ℤ) :
a ^ (1 + i) = a * a ^ i
source
theorem zsmul_add_comm {G : Type w} [add_group G] (a : G) (i j : ℤ) :
i • a + j • a = j • a + i • a
source
theorem zpow_mul_comm {G : Type w} [group G] (a : G) (i j : ℤ) :
a ^ i * a ^ j = a ^ j * a ^ i
source
theorem zpow_bit1 {G : Type w} [group G] (a : G) (n : ℤ) :
a ^ bit1 n = a ^ n * a ^ n * a
source
theorem bit1_zsmul {G : Type w} [add_group G] (a : G) (n : ℤ) :
bit1 n • a = n • a + n • a + a
source
theorem zsmul_induction_left {G : Type w} [add_group G] {g : G} {P : G → Prop} (h_one : P 0) (h_mul : ∀ (a : G), P a → P (g + a)) (h_inv : ∀ (a : G), P a → P (-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 add_subgroup.closure_induction_left.

source
theorem zpow_induction_left {G : Type w} [group G] {g : G} {P : G → Prop} (h_one : P 1) (h_mul : ∀ (a : G), P a → P (g * a)) (h_inv : ∀ (a : G), P a → P (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.

source
theorem zsmul_induction_right {G : Type w} [add_group G] {g : G} {P : G → Prop} (h_one : P 0) (h_mul : ∀ (a : G), P a → P (a + g)) (h_inv : ∀ (a : G), P a → P (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 add_subgroup.closure_induction_right.

source
theorem zpow_induction_right {G : Type w} [group G] {g : G} {P : G → Prop} (h_one : P 1) (h_mul : ∀ (a : G), P a → P (a * g)) (h_inv : ∀ (a : G), P a → P (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.

zpow/zsmul and an order #

Those lemmas are placed here (rather than in algebra.group_power.order with their friends) because they require facts from data.int.basic.

source
theorem one_lt_zpow' {α : Type u_1} [ordered_comm_group α] {a : α} (ha : 1 < a) {k : ℤ} (hk : 0 < k) :
1 < a ^ k
source
theorem zsmul_pos {α : Type u_1} [ordered_add_comm_group α] {a : α} (ha : 0 < a) {k : ℤ} (hk : 0 < k) :
0 < k • a
source
theorem zsmul_strict_mono_left {α : Type u_1} [ordered_add_comm_group α] {a : α} (ha : 0 < a) :
strict_mono (λ (n : ℤ), n • a)
source
theorem zpow_strict_mono_right {α : Type u_1} [ordered_comm_group α] {a : α} (ha : 1 < a) :
strict_mono (λ (n : ℤ), a ^ n)
source
theorem zsmul_mono_left {α : Type u_1} [ordered_add_comm_group α] {a : α} (ha : 0 ≤ a) :
monotone (λ (n : ℤ), n • a)
source
theorem zpow_mono_right {α : Type u_1} [ordered_comm_group α] {a : α} (ha : 1 ≤ a) :
monotone (λ (n : ℤ), a ^ n)
source
theorem zsmul_le_zsmul {α : Type u_1} [ordered_add_comm_group α] {m n : ℤ} {a : α} (ha : 0 ≤ a) (h : m ≤ n) :
m • a ≤ n • a
source
theorem zpow_le_zpow {α : Type u_1} [ordered_comm_group α] {m n : ℤ} {a : α} (ha : 1 ≤ a) (h : m ≤ n) :
a ^ m ≤ a ^ n
source
theorem zsmul_lt_zsmul {α : Type u_1} [ordered_add_comm_group α] {m n : ℤ} {a : α} (ha : 0 < a) (h : m < n) :
m • a < n • a
source
theorem zpow_lt_zpow {α : Type u_1} [ordered_comm_group α] {m n : ℤ} {a : α} (ha : 1 < a) (h : m < n) :
a ^ m < a ^ n
source
theorem zsmul_le_zsmul_iff {α : Type u_1} [ordered_add_comm_group α] {m n : ℤ} {a : α} (ha : 0 < a) :
m • a ≤ n • a ↔ m ≤ n
source
theorem zpow_le_zpow_iff {α : Type u_1} [ordered_comm_group α] {m n : ℤ} {a : α} (ha : 1 < a) :
a ^ m ≤ a ^ n ↔ m ≤ n
source
theorem zpow_lt_zpow_iff {α : Type u_1} [ordered_comm_group α] {m n : ℤ} {a : α} (ha : 1 < a) :
a ^ m < a ^ n ↔ m < n
source
theorem zsmul_lt_zsmul_iff {α : Type u_1} [ordered_add_comm_group α] {m n : ℤ} {a : α} (ha : 0 < a) :
m • a < n • a ↔ m < n
source
theorem zsmul_strict_mono_right (α : Type u_1) [ordered_add_comm_group α] {n : ℤ} (hn : 0 < n) :
strict_mono (λ (_x : α), n • _x)
source
theorem zpow_strict_mono_left (α : Type u_1) [ordered_comm_group α] {n : ℤ} (hn : 0 < n) :
strict_mono (λ (_x : α), _x ^ n)
source
theorem zpow_mono_left (α : Type u_1) [ordered_comm_group α] {n : ℤ} (hn : 0 ≤ n) :
monotone (λ (_x : α), _x ^ n)
source
theorem zsmul_mono_right (α : Type u_1) [ordered_add_comm_group α] {n : ℤ} (hn : 0 ≤ n) :
monotone (λ (_x : α), n • _x)
source
theorem zpow_le_zpow' {α : Type u_1} [ordered_comm_group α] {n : ℤ} {a b : α} (hn : 0 ≤ n) (h : a ≤ b) :
a ^ n ≤ b ^ n
source
theorem zsmul_le_zsmul' {α : Type u_1} [ordered_add_comm_group α] {n : ℤ} {a b : α} (hn : 0 ≤ n) (h : a ≤ b) :
n • a ≤ n • b
source
theorem zsmul_lt_zsmul' {α : Type u_1} [ordered_add_comm_group α] {n : ℤ} {a b : α} (hn : 0 < n) (h : a < b) :
n • a < n • b
source
theorem zpow_lt_zpow' {α : Type u_1} [ordered_comm_group α] {n : ℤ} {a b : α} (hn : 0 < n) (h : a < b) :
a ^ n < b ^ n
source
theorem zsmul_le_zsmul_iff' {α : Type u_1} [linear_ordered_add_comm_group α] {n : ℤ} (hn : 0 < n) {a b : α} :
n • a ≤ n • b ↔ a ≤ b
source
theorem zpow_le_zpow_iff' {α : Type u_1} [linear_ordered_comm_group α] {n : ℤ} (hn : 0 < n) {a b : α} :
a ^ n ≤ b ^ n ↔ a ≤ b
source
theorem zpow_lt_zpow_iff' {α : Type u_1} [linear_ordered_comm_group α] {n : ℤ} (hn : 0 < n) {a b : α} :
a ^ n < b ^ n ↔ a < b
source
theorem zsmul_lt_zsmul_iff' {α : Type u_1} [linear_ordered_add_comm_group α] {n : ℤ} (hn : 0 < n) {a b : α} :
n • a < n • b ↔ a < b
source
@[nolint]
theorem zpow_left_injective {α : Type u_1} [linear_ordered_comm_group α] {n : ℤ} (hn : n ≠ 0) :
function.injective (λ (_x : α), _x ^ n)
source
@[nolint]
theorem zsmul_right_injective {α : Type u_1} [linear_ordered_add_comm_group α] {n : ℤ} (hn : n ≠ 0) :
function.injective (λ (_x : α), n • _x)

See also smul_right_injective. TODO: provide a no_zero_smul_divisors instance. We can't do that here because importing that definition would create import cycles.

source
theorem zsmul_right_inj {α : Type u_1} [linear_ordered_add_comm_group α] {n : ℤ} {a b : α} (hn : n ≠ 0) :
n • a = n • b ↔ a = b
source
theorem zpow_left_inj {α : Type u_1} [linear_ordered_comm_group α] {n : ℤ} {a b : α} (hn : n ≠ 0) :
a ^ n = b ^ n ↔ a = b
source
theorem zpow_eq_zpow_iff' {α : Type u_1} [linear_ordered_comm_group α] {n : ℤ} {a b : α} (hn : n ≠ 0) :
a ^ n = b ^ n ↔ a = b

Alias of zsmul_right_inj, for ease of discovery alongside zsmul_le_zsmul_iff' and zsmul_lt_zsmul_iff'.

source
theorem zsmul_eq_zsmul_iff' {α : Type u_1} [linear_ordered_add_comm_group α] {n : ℤ} {a b : α} (hn : n ≠ 0) :
n • a = n • b ↔ a = b

Alias of zsmul_right_inj, for ease of discovery alongside zsmul_le_zsmul_iff' and zsmul_lt_zsmul_iff'.

source
theorem abs_nsmul {α : Type u_1} [linear_ordered_add_comm_group α] (n : ℕ) (a : α) :
|n • a| = n • |a|
source
theorem abs_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] (n : ℤ) (a : α) :
|n • a| = |n| • |a|
source
theorem abs_add_eq_add_abs_le {α : Type u_1} [linear_ordered_add_comm_group α] {a b : α} (hle : a ≤ b) :
|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
source
theorem abs_add_eq_add_abs_iff {α : Type u_1} [linear_ordered_add_comm_group α] (a b : α) :
|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
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₁} [non_assoc_semiring R] (a : R) (n : ℕ) :
n • a = a * ↑n
source
@[simp]
theorem nsmul_eq_mul {R : Type u₁} [non_assoc_semiring R] (n : ℕ) (a : R) :
n • a = ↑n * a
source
@[protected, instance]
def non_unital_non_assoc_semiring.nat_smul_comm_class {R : Type u₁} [non_unital_non_assoc_semiring R] :
smul_comm_class ℕ R R

Note that add_comm_monoid.nat_smul_comm_class requires stronger assumptions on R.

source
@[protected, instance]
def non_unital_non_assoc_semiring.nat_is_scalar_tower {R : Type u₁} [non_unital_non_assoc_semiring R] :
is_scalar_tower ℕ R R

Note that add_comm_monoid.nat_is_scalar_tower requires stronger assumptions on R.

source
@[simp, norm_cast]
theorem nat.cast_pow {R : Type u₁} [semiring R] (n m : ℕ) :
↑(n ^ m) = ↑n ^ m
source
@[simp, norm_cast]
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
theorem bit0_mul {R : Type u₁} [non_unital_non_assoc_ring R] {n r : R} :
bit0 n * r = 2 • (n * r)
source
theorem mul_bit0 {R : Type u₁} [non_unital_non_assoc_ring R] {n r : R} :
r * bit0 n = 2 • (r * n)
source
theorem bit1_mul {R : Type u₁} [non_assoc_ring R] {n r : R} :
bit1 n * r = 2 • (n * r) + r
source
theorem mul_bit1 {R : Type u₁} [non_assoc_ring R] {n r : R} :
r * bit1 n = 2 • (r * n) + r
source
theorem int.cast_mul_eq_zsmul_cast {α : Type u_1} [add_comm_group_with_one α] (m n : ℤ) :
↑(m * n) = m • ↑n

Note this holds in marginally more generality than int.cast_mul

source
@[simp]
theorem zsmul_eq_mul {R : Type u₁} [ring R] (a : R) (n : ℤ) :
n • a = ↑n * a
source
theorem zsmul_eq_mul' {R : Type u₁} [ring R] (a : R) (n : ℤ) :
n • a = a * ↑n
source
@[protected, instance]
def non_unital_non_assoc_ring.int_smul_comm_class {R : Type u₁} [non_unital_non_assoc_ring R] :
smul_comm_class ℤ R R

Note that add_comm_group.int_smul_comm_class requires stronger assumptions on R.

source
@[protected, instance]
def non_unital_non_assoc_ring.int_is_scalar_tower {R : Type u₁} [non_unital_non_assoc_ring R] :
is_scalar_tower ℤ R R

Note that add_comm_group.int_is_scalar_tower requires stronger assumptions on R.

source
theorem zsmul_int_int (a b : ℤ) :
a • b = a * b
source
theorem zsmul_int_one (n : ℤ) :
n • 1 = n
source
@[simp, norm_cast]
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 one_add_mul_le_pow' {R : Type u₁} [strict_ordered_semiring R] {a : R} (Hsq : 0 ≤ a * a) (Hsq' : 0 ≤ (1 + a) * (1 + a)) (H : 0 ≤ 2 + a) (n : ℕ) :
1 + ↑n * a ≤ (1 + a) ^ n

Bernoulli's inequality. This version works for semirings but requires additional hypotheses 0 ≤ a * a and 0 ≤ (1 + a) * (1 + a).

source
theorem pow_le_pow_of_le_one {R : Type u₁} [strict_ordered_semiring R] {a : R} (h : 0 ≤ a) (ha : a ≤ 1) {i j : ℕ} (hij : i ≤ j) :
a ^ j ≤ a ^ i
source
theorem pow_le_of_le_one {R : Type u₁} [strict_ordered_semiring R] {a : R} (h₀ : 0 ≤ a) (h₁ : a ≤ 1) {n : ℕ} (hn : n ≠ 0) :
a ^ n ≤ a
source
theorem sq_le {R : Type u₁} [strict_ordered_semiring R] {a : R} (h₀ : 0 ≤ a) (h₁ : a ≤ 1) :
a ^ 2 ≤ a
source
theorem sign_cases_of_C_mul_pow_nonneg {R : Type u₁} [linear_ordered_semiring R] {C r : R} (h : ∀ (n : ℕ), 0 ≤ C * r ^ n) :
C = 0 ∨ 0 < C ∧ 0 ≤ r
source
@[simp]
theorem abs_pow {R : Type u₁} [linear_ordered_ring R] (a : R) (n : ℕ) :
|a ^ n| = |a| ^ n
source
@[simp]
theorem pow_bit1_neg_iff {R : Type u₁} [linear_ordered_ring R] {a : R} {n : ℕ} :
a ^ bit1 n < 0 ↔ a < 0
source
@[simp]
theorem pow_bit1_nonneg_iff {R : Type u₁} [linear_ordered_ring R] {a : R} {n : ℕ} :
0 ≤ a ^ bit1 n ↔ 0 ≤ a
source
@[simp]
theorem pow_bit1_nonpos_iff {R : Type u₁} [linear_ordered_ring R] {a : R} {n : ℕ} :
a ^ bit1 n ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem pow_bit1_pos_iff {R : Type u₁} [linear_ordered_ring R] {a : R} {n : ℕ} :
0 < a ^ bit1 n ↔ 0 < a
source
theorem strict_mono_pow_bit1 {R : Type u₁} [linear_ordered_ring R] (n : ℕ) :
strict_mono (λ (a : R), a ^ bit1 n)
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_mul_sub_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.nat_abs_sq (x : ℤ) :
↑(x.nat_abs) ^ 2 = x ^ 2
source
theorem int.nat_abs_pow_two (x : ℤ) :
↑(x.nat_abs) ^ 2 = x ^ 2

Alias of int.nat_abs_sq.

source
theorem int.abs_le_self_sq (a : ℤ) :
↑(a.nat_abs) ≤ a ^ 2
source
theorem int.abs_le_self_pow_two (a : ℤ) :
↑(a.nat_abs) ≤ a ^ 2

Alias of int.abs_le_self_sq.

source
theorem int.le_self_sq (b : ℤ) :
b ≤ b ^ 2
source
theorem int.le_self_pow_two (b : ℤ) :
b ≤ b ^ 2

Alias of int.le_self_sq.

source
theorem int.pow_right_injective {x : ℤ} (h : 1 < x.nat_abs) :
function.injective (has_pow.pow x)
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
source
def zpowers_hom (G : Type w) [group G] :
G ≃ (multiplicative ℤ →* G)

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

Equations
source
def multiples_hom (A : Type y) [add_monoid A] :
A ≃ (ℕ →+ A)

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

Equations
source
def zmultiples_hom (A : Type y) [add_group A] :
A ≃ (ℤ →+ A)

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

Equations
source
@[simp]
theorem powers_hom_apply {M : Type u} [monoid M] (x : M) (n : multiplicative ℕ) :
⇑(⇑(powers_hom M) x) n = x ^ ⇑multiplicative.to_add n
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
@[simp]
theorem zpowers_hom_apply {G : Type w} [group G] (x : G) (n : multiplicative ℤ) :
⇑(⇑(zpowers_hom G) x) n = x ^ ⇑multiplicative.to_add n
source
@[simp]
theorem zpowers_hom_symm_apply {G : Type w} [group G] (f : multiplicative ℤ →* G) :
⇑((zpowers_hom G).symm) f = ⇑f (⇑multiplicative.of_add 1)
source
@[simp]
theorem multiples_hom_apply {A : Type y} [add_monoid A] (x : A) (n : ℕ) :
⇑(⇑(multiples_hom A) x) n = n • x
source
@[simp]
theorem multiples_hom_symm_apply {A : Type y} [add_monoid A] (f : ℕ →+ A) :
⇑((multiples_hom A).symm) f = ⇑f 1
source
@[simp]
theorem zmultiples_hom_apply {A : Type y} [add_group A] (x : A) (n : ℤ) :
⇑(⇑(zmultiples_hom A) x) n = n • x
source
@[simp]
theorem zmultiples_hom_symm_apply {A : Type y} [add_group A] (f : ℤ →+ A) :
⇑((zmultiples_hom A).symm) f = ⇑f 1
source
theorem monoid_hom.apply_mnat {M : Type u} [monoid M] (f : multiplicative ℕ →* M) (n : multiplicative ℕ) :
⇑f n = ⇑f (⇑multiplicative.of_add 1) ^ ⇑multiplicative.to_add n
source
@[ext]
theorem monoid_hom.ext_mnat {M : Type u} [monoid M] ⦃f g : multiplicative ℕ →* M⦄ (h : ⇑f (⇑multiplicative.of_add 1) = ⇑g (⇑multiplicative.of_add 1)) :
f = g
source
theorem monoid_hom.apply_mint {M : Type u} [group M] (f : multiplicative ℤ →* M) (n : multiplicative ℤ) :
⇑f n = ⇑f (⇑multiplicative.of_add 1) ^ ⇑multiplicative.to_add n

monoid_hom.ext_mint is defined in data.int.cast

source
theorem add_monoid_hom.apply_nat {M : Type u} [add_monoid M] (f : ℕ →+ M) (n : ℕ) :
⇑f n = n • ⇑f 1

add_monoid_hom.ext_nat is defined in data.nat.cast

source
theorem add_monoid_hom.apply_int {M : Type u} [add_group M] (f : ℤ →+ M) (n : ℤ) :
⇑f n = n • ⇑f 1

add_monoid_hom.ext_int is defined in data.int.cast

source
def powers_mul_hom (M : Type u) [comm_monoid M] :
M ≃* (multiplicative ℕ →* M)

If M is commutative, powers_hom is a multiplicative equivalence.

Equations
source
def zpowers_mul_hom (G : Type w) [comm_group G] :
G ≃* (multiplicative ℤ →* G)

If M is commutative, zpowers_hom is a multiplicative equivalence.

Equations
source
def multiples_add_hom (A : Type y) [add_comm_monoid A] :
A ≃+ (ℕ →+ A)

If M is commutative, multiples_hom is an additive equivalence.

Equations
source
def zmultiples_add_hom (A : Type y) [add_comm_group A] :
A ≃+ (ℤ →+ A)

If M is commutative, zmultiples_hom is an additive equivalence.

Equations
source
@[simp]
theorem powers_mul_hom_apply {M : Type u} [comm_monoid M] (x : M) (n : multiplicative ℕ) :
⇑(⇑(powers_mul_hom M) x) n = x ^ ⇑multiplicative.to_add n
source
@[simp]
theorem powers_mul_hom_symm_apply {M : Type u} [comm_monoid M] (f : multiplicative ℕ →* M) :
⇑((powers_mul_hom M).symm) f = ⇑f (⇑multiplicative.of_add 1)
source
@[simp]
theorem zpowers_mul_hom_apply {G : Type w} [comm_group G] (x : G) (n : multiplicative ℤ) :
⇑(⇑(zpowers_mul_hom G) x) n = x ^ ⇑multiplicative.to_add n
source
@[simp]
theorem zpowers_mul_hom_symm_apply {G : Type w} [comm_group G] (f : multiplicative ℤ →* G) :
⇑((zpowers_mul_hom G).symm) f = ⇑f (⇑multiplicative.of_add 1)
source
@[simp]
theorem multiples_add_hom_apply {A : Type y} [add_comm_monoid A] (x : A) (n : ℕ) :
⇑(⇑(multiples_add_hom A) x) n = n • x
source
@[simp]
theorem multiples_add_hom_symm_apply {A : Type y} [add_comm_monoid A] (f : ℕ →+ A) :
⇑((multiples_add_hom A).symm) f = ⇑f 1
source
@[simp]
theorem zmultiples_add_hom_apply {A : Type y} [add_comm_group A] (x : A) (n : ℤ) :
⇑(⇑(zmultiples_add_hom A) x) n = n • x
source
@[simp]
theorem zmultiples_add_hom_symm_apply {A : Type y} [add_comm_group A] (f : ℤ →+ A) :
⇑((zmultiples_add_hom A).symm) f = ⇑f 1

Commutativity (again) #

Facts about semiconj_by and commute that require zpow or zsmul, or the fact that integer multiplication equals semiring multiplication.

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 add_semiconj_by.add_units_zsmul_right {M : Type u} [add_monoid M] {a : M} {x y : add_units M} (h : add_semiconj_by a ↑x ↑y) (m : ℤ) :
add_semiconj_by a ↑(m • x) ↑(m • y)
source
@[simp]
theorem semiconj_by.units_zpow_right {M : Type u} [monoid M] {a : M} {x y : Mˣ} (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_zpow_right {M : Type u} [monoid M] {a : M} {u : Mˣ} (h : commute a ↑u) (m : ℤ) :
commute a ↑(u ^ m)
source
@[simp]
theorem add_commute.add_units_zsmul_right {M : Type u} [add_monoid M] {a : M} {u : add_units M} (h : add_commute a ↑u) (m : ℤ) :
add_commute a ↑(m • u)
source
@[simp]
theorem commute.units_zpow_left {M : Type u} [monoid M] {u : Mˣ} {a : M} (h : commute ↑u a) (m : ℤ) :
commute ↑(u ^ m) a
source
@[simp]
theorem add_commute.add_units_zsmul_left {M : Type u} [add_monoid M] {u : add_units M} {a : M} (h : add_commute ↑u a) (m : ℤ) :
add_commute ↑(m • u) a
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.cast_int_left {R : Type u₁} [ring R] (a : R) (m : ℤ) :
commute ↑m a
source
@[simp]
theorem commute.cast_int_right {R : Type u₁} [ring R] (a : R) (m : ℤ) :
commute a ↑m
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 : ℕ) :
⇑multiplicative.to_add (a ^ b) = ⇑multiplicative.to_add a * 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 : ℕ) :
⇑multiplicative.to_add (a ^ b) = ⇑multiplicative.to_add a * ↑b
source
@[simp]
theorem int.to_add_zpow (a : multiplicative ℤ) (b : ℤ) :
⇑multiplicative.to_add (a ^ b) = ⇑multiplicative.to_add a * 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 : Mˣ) (x : M) (n : ℕ) :
(↑u * x * ↑u⁻¹) ^ n = ↑u * x ^ n * ↑u⁻¹
source
theorem units.conj_pow' {M : Type u} [monoid M] (u : Mˣ) (x : M) (n : ℕ) :
(↑u⁻¹ * x * ↑u) ^ n = ↑u⁻¹ * x ^ n * ↑u
source
@[simp]
theorem mul_opposite.op_pow {M : Type u} [monoid M] (x : M) (n : ℕ) :
mul_opposite.op (x ^ n) = mul_opposite.op x ^ n

Moving to the opposite monoid commutes with taking powers.

source
@[simp]
theorem mul_opposite.unop_pow {M : Type u} [monoid M] (x : Mᵐᵒᵖ) (n : ℕ) :
mul_opposite.unop (x ^ n) = mul_opposite.unop x ^ n
source
@[simp]
theorem mul_opposite.op_zpow {M : Type u} [div_inv_monoid M] (x : M) (z : ℤ) :
mul_opposite.op (x ^ z) = mul_opposite.op x ^ z

Moving to the opposite group or group_with_zero commutes with taking powers.

source
@[simp]
theorem mul_opposite.unop_zpow {M : Type u} [div_inv_monoid M] (x : Mᵐᵒᵖ) (z : ℤ) :
mul_opposite.unop (x ^ z) = mul_opposite.unop x ^ z