# mathlib3documentation

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

@[simp]
theorem nsmul_one {A : Type y} (n : ) :
n 1 = n
@[protected, instance]
def invertible_pow {M : Type u} [monoid M] (m : M) [invertible m] (n : ) :
Equations
theorem inv_of_pow {M : Type u} [monoid M] (m : M) [invertible m] (n : ) [invertible (m ^ n)] :
(m ^ n) = m ^ n
theorem is_add_unit.nsmul {M : Type u} [add_monoid M] {m : M} (n : ) :
theorem is_unit.pow {M : Type u} [monoid M] {m : M} (n : ) :
is_unit (m ^ n)
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) :

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

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

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

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

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

Equations
@[simp]
theorem units.coe_of_pow_eq_one {M : Type u} [monoid M] (x : M) (n : ) (hx : x ^ n = 1) (hn : n 0) :
hx hn) = x
@[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) :
- hn = (n - 1) x
def units.of_pow_eq_one {M : Type u} [monoid M] (x : M) (n : ) (hx : x ^ n = 1) (hn : n 0) :

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

Equations
@[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) :
hx hn) = x
@[simp]
theorem units.pow_of_pow_eq_one {M : Type u} [monoid M] {x : M} {n : } (hx : x ^ n = 1) (hn : n 0) :
hx hn ^ n = 1
@[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 hn = 0
theorem is_add_unit_of_nsmul_eq_zero {M : Type u} [add_monoid M] {x : M} {n : } (hx : n x = 0) (hn : n 0) :
theorem is_unit_of_pow_eq_one {M : Type u} [monoid M] {x : M} {n : } (hx : x ^ n = 1) (hn : n 0) :
def invertible_of_pow_eq_one {M : Type u} [monoid M] (x : M) (n : ) (hx : x ^ n = 1) (hn : n 0) :

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

Equations
theorem smul_pow {M : Type u} {N : Type v} [monoid M] [monoid N] [ N] [ N] [ N] (k : M) (x : N) (p : ) :
(k x) ^ p = k ^ p x ^ p
@[simp]
theorem smul_pow' {M : Type u} {N : Type v} [monoid M] [monoid N] (x : M) (m : N) (n : ) :
x m ^ n = (x m) ^ n
theorem zsmul_one {A : Type y} (n : ) :
n 1 = n
theorem mul_zsmul' {α : Type u_1} (a : α) (m n : ) :
(m * n) a = n m a
theorem zpow_mul {α : Type u_1} (a : α) (m n : ) :
a ^ (m * n) = (a ^ m) ^ n
theorem zpow_mul' {α : Type u_1} (a : α) (m n : ) :
a ^ (m * n) = (a ^ n) ^ m
theorem mul_zsmul {α : Type u_1} (a : α) (m n : ) :
(m * n) a = m n a
theorem bit0_zsmul {α : Type u_1} (a : α) (n : ) :
bit0 n a = n a + n a
theorem zpow_bit0 {α : Type u_1} (a : α) (n : ) :
a ^ bit0 n = a ^ n * a ^ n
theorem zpow_bit0' {α : Type u_1} (a : α) (n : ) :
a ^ bit0 n = (a * a) ^ n
theorem bit0_zsmul' {α : Type u_1} (a : α) (n : ) :
bit0 n a = n (a + a)
@[simp]
theorem zpow_bit0_neg {α : Type u_1} (x : α) (n : ) :
(-x) ^ bit0 n = x ^ bit0 n
theorem zpow_add_one {G : Type w} [group G] (a : G) (n : ) :
a ^ (n + 1) = a ^ n * a
theorem add_one_zsmul {G : Type w} [add_group G] (a : G) (n : ) :
(n + 1) a = n a + a
theorem sub_one_zsmul {G : Type w} [add_group 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 zpow_add {G : Type w} [group G] (a : G) (m n : ) :
a ^ (m + n) = a ^ m * a ^ n
theorem add_zsmul {G : Type w} [add_group G] (a : G) (m n : ) :
(m + n) a = m a + n a
theorem mul_self_zpow {G : Type w} [group G] (b : G) (m : ) :
b * b ^ m = b ^ (m + 1)
theorem add_zsmul_self {G : Type w} [add_group G] (b : G) (m : ) :
b + m b = (m + 1) b
theorem add_self_zsmul {G : Type w} [add_group G] (b : G) (m : ) :
m b + b = (m + 1) b
theorem mul_zpow_self {G : Type w} [group G] (b : G) (m : ) :
b ^ m * b = b ^ (m + 1)
theorem sub_zsmul {G : Type w} [add_group 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 one_add_zsmul {G : Type w} [add_group G] (a : G) (i : ) :
(1 + i) a = a + i a
theorem zpow_one_add {G : Type w} [group G] (a : G) (i : ) :
a ^ (1 + i) = a * a ^ i
theorem zsmul_add_comm {G : Type w} [add_group G] (a : G) (i j : ) :
i a + j a = j a + i a
theorem zpow_mul_comm {G : Type w} [group G] (a : G) (i j : ) :
a ^ i * a ^ j = a ^ j * a ^ i
theorem zpow_bit1 {G : Type w} [group G] (a : G) (n : ) :
a ^ bit1 n = a ^ n * a ^ n * a
theorem bit1_zsmul {G : Type w} [add_group G] (a : G) (n : ) :
bit1 n a = n a + n a + a
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`.

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

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

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

theorem one_lt_zpow' {α : Type u_1} {a : α} (ha : 1 < a) {k : } (hk : 0 < k) :
1 < a ^ k
theorem zsmul_pos {α : Type u_1} {a : α} (ha : 0 < a) {k : } (hk : 0 < k) :
0 < k a
theorem zsmul_strict_mono_left {α : Type u_1} {a : α} (ha : 0 < a) :
strict_mono (λ (n : ), n a)
theorem zpow_strict_mono_right {α : Type u_1} {a : α} (ha : 1 < a) :
strict_mono (λ (n : ), a ^ n)
theorem zsmul_mono_left {α : Type u_1} {a : α} (ha : 0 a) :
monotone (λ (n : ), n a)
theorem zpow_mono_right {α : Type u_1} {a : α} (ha : 1 a) :
monotone (λ (n : ), a ^ n)
theorem zsmul_le_zsmul {α : Type u_1} {m n : } {a : α} (ha : 0 a) (h : m n) :
m a n a
theorem zpow_le_zpow {α : Type u_1} {m n : } {a : α} (ha : 1 a) (h : m n) :
a ^ m a ^ n
theorem zsmul_lt_zsmul {α : Type u_1} {m n : } {a : α} (ha : 0 < a) (h : m < n) :
m a < n a
theorem zpow_lt_zpow {α : Type u_1} {m n : } {a : α} (ha : 1 < a) (h : m < n) :
a ^ m < a ^ n
theorem zsmul_le_zsmul_iff {α : Type u_1} {m n : } {a : α} (ha : 0 < a) :
m a n a m n
theorem zpow_le_zpow_iff {α : Type u_1} {m n : } {a : α} (ha : 1 < a) :
a ^ m a ^ n m n
theorem zpow_lt_zpow_iff {α : Type u_1} {m n : } {a : α} (ha : 1 < a) :
a ^ m < a ^ n m < n
theorem zsmul_lt_zsmul_iff {α : Type u_1} {m n : } {a : α} (ha : 0 < a) :
m a < n a m < n
theorem zsmul_strict_mono_right (α : Type u_1) {n : } (hn : 0 < n) :
strict_mono (λ (_x : α), n _x)
theorem zpow_strict_mono_left (α : Type u_1) {n : } (hn : 0 < n) :
strict_mono (λ (_x : α), _x ^ n)
theorem zpow_mono_left (α : Type u_1) {n : } (hn : 0 n) :
monotone (λ (_x : α), _x ^ n)
theorem zsmul_mono_right (α : Type u_1) {n : } (hn : 0 n) :
monotone (λ (_x : α), n _x)
theorem zpow_le_zpow' {α : Type u_1} {n : } {a b : α} (hn : 0 n) (h : a b) :
a ^ n b ^ n
theorem zsmul_le_zsmul' {α : Type u_1} {n : } {a b : α} (hn : 0 n) (h : a b) :
n a n b
theorem zsmul_lt_zsmul' {α : Type u_1} {n : } {a b : α} (hn : 0 < n) (h : a < b) :
n a < n b
theorem zpow_lt_zpow' {α : Type u_1} {n : } {a b : α} (hn : 0 < n) (h : a < b) :
a ^ n < b ^ n
theorem zsmul_le_zsmul_iff' {α : Type u_1} {n : } (hn : 0 < n) {a b : α} :
n a n b a b
theorem zpow_le_zpow_iff' {α : Type u_1} {n : } (hn : 0 < n) {a b : α} :
a ^ n b ^ n a b
theorem zpow_lt_zpow_iff' {α : Type u_1} {n : } (hn : 0 < n) {a b : α} :
a ^ n < b ^ n a < b
theorem zsmul_lt_zsmul_iff' {α : Type u_1} {n : } (hn : 0 < n) {a b : α} :
n a < n b a < b
@[nolint]
theorem zpow_left_injective {α : Type u_1} {n : } (hn : n 0) :
function.injective (λ (_x : α), _x ^ n)
@[nolint]
theorem zsmul_right_injective {α : Type u_1} {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.

theorem zsmul_right_inj {α : Type u_1} {n : } {a b : α} (hn : n 0) :
n a = n b a = b
theorem zpow_left_inj {α : Type u_1} {n : } {a b : α} (hn : n 0) :
a ^ n = b ^ n a = b
theorem zpow_eq_zpow_iff' {α : Type u_1} {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'`.

theorem zsmul_eq_zsmul_iff' {α : Type u_1} {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'`.

theorem abs_nsmul {α : Type u_1} (n : ) (a : α) :
|n a| = n |a|
theorem abs_zsmul {α : Type u_1} (n : ) (a : α) :
|n a| = |n| |a|
theorem abs_add_eq_add_abs_le {α : Type u_1} {a b : α} (hle : a b) :
|a + b| = |a| + |b| 0 a 0 b a 0 b 0
|a + b| = |a| + |b| 0 a 0 b a 0 b 0
@[simp]
theorem with_bot.coe_nsmul {A : Type y} [add_monoid A] (a : A) (n : ) :
(n a) = n a
theorem nsmul_eq_mul' {R : Type u₁} (a : R) (n : ) :
n a = a * n
@[simp]
theorem nsmul_eq_mul {R : Type u₁} (n : ) (a : R) :
n a = n * a
@[protected, instance]

Note that `add_comm_monoid.nat_smul_comm_class` requires stronger assumptions on `R`.

@[protected, instance]

Note that `add_comm_monoid.nat_is_scalar_tower` requires stronger assumptions on `R`.

@[simp, norm_cast]
theorem nat.cast_pow {R : Type u₁} [semiring R] (n m : ) :
(n ^ m) = n ^ m
@[simp, norm_cast]
theorem int.coe_nat_pow (n m : ) :
(n ^ m) = n ^ m
theorem int.nat_abs_pow (n : ) (k : ) :
(n ^ k).nat_abs = n.nat_abs ^ k
theorem bit0_mul {R : Type u₁} {n r : R} :
bit0 n * r = 2 (n * r)
theorem mul_bit0 {R : Type u₁} {n r : R} :
r * bit0 n = 2 (r * n)
theorem bit1_mul {R : Type u₁} {n r : R} :
bit1 n * r = 2 (n * r) + r
theorem mul_bit1 {R : Type u₁} {n r : R} :
r * bit1 n = 2 (r * n) + r
theorem int.cast_mul_eq_zsmul_cast {α : Type u_1} (m n : ) :
(m * n) = m n

Note this holds in marginally more generality than `int.cast_mul`

@[simp]
theorem zsmul_eq_mul {R : Type u₁} [ring R] (a : R) (n : ) :
n a = n * a
theorem zsmul_eq_mul' {R : Type u₁} [ring R] (a : R) (n : ) :
n a = a * n
@[protected, instance]

Note that `add_comm_group.int_smul_comm_class` requires stronger assumptions on `R`.

@[protected, instance]

Note that `add_comm_group.int_is_scalar_tower` requires stronger assumptions on `R`.

theorem zsmul_int_int (a b : ) :
a b = a * b
theorem zsmul_int_one (n : ) :
n 1 = n
@[simp, norm_cast]
theorem int.cast_pow {R : Type u₁} [ring R] (n : ) (m : ) :
(n ^ m) = n ^ m
theorem neg_one_pow_eq_pow_mod_two {R : Type u₁} [ring R] {n : } :
(-1) ^ n = (-1) ^ (n % 2)
theorem one_add_mul_le_pow' {R : Type u₁} {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)`.

theorem pow_le_pow_of_le_one {R : Type u₁} {a : R} (h : 0 a) (ha : a 1) {i j : } (hij : i j) :
a ^ j a ^ i
theorem pow_le_of_le_one {R : Type u₁} {a : R} (h₀ : 0 a) (h₁ : a 1) {n : } (hn : n 0) :
a ^ n a
theorem sq_le {R : Type u₁} {a : R} (h₀ : 0 a) (h₁ : a 1) :
a ^ 2 a
theorem sign_cases_of_C_mul_pow_nonneg {R : Type u₁} {C r : R} (h : (n : ), 0 C * r ^ n) :
C = 0 0 < C 0 r
@[simp]
theorem abs_pow {R : Type u₁} (a : R) (n : ) :
|a ^ n| = |a| ^ n
@[simp]
theorem pow_bit1_neg_iff {R : Type u₁} {a : R} {n : } :
a ^ bit1 n < 0 a < 0
@[simp]
theorem pow_bit1_nonneg_iff {R : Type u₁} {a : R} {n : } :
0 a ^ bit1 n 0 a
@[simp]
theorem pow_bit1_nonpos_iff {R : Type u₁} {a : R} {n : } :
a ^ bit1 n 0 a 0
@[simp]
theorem pow_bit1_pos_iff {R : Type u₁} {a : R} {n : } :
0 < a ^ bit1 n 0 < a
theorem strict_mono_pow_bit1 {R : Type u₁} (n : ) :
strict_mono (λ (a : R), a ^ bit1 n)
theorem one_add_mul_le_pow {R : Type u₁} {a : R} (H : -2 a) (n : ) :
1 + n * a (1 + a) ^ n

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

theorem one_add_mul_sub_le_pow {R : Type u₁} {a : R} (H : -1 a) (n : ) :
1 + n * (a - 1) a ^ n

Bernoulli's inequality reformulated to estimate `a^n`.

theorem int.nat_abs_sq (x : ) :
(x.nat_abs) ^ 2 = x ^ 2
theorem int.nat_abs_pow_two (x : ) :
(x.nat_abs) ^ 2 = x ^ 2

Alias of `int.nat_abs_sq`.

theorem int.abs_le_self_sq (a : ) :
(a.nat_abs) a ^ 2
theorem int.abs_le_self_pow_two (a : ) :
(a.nat_abs) a ^ 2

Alias of `int.abs_le_self_sq`.

theorem int.le_self_sq (b : ) :
b b ^ 2
theorem int.le_self_pow_two (b : ) :
b b ^ 2

Alias of `int.le_self_sq`.

theorem int.pow_right_injective {x : } (h : 1 < x.nat_abs) :
def powers_hom (M : Type u) [monoid M] :
M

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

Equations
def zpowers_hom (G : Type w) [group G] :
G

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

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

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

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

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

Equations
@[simp]
theorem powers_hom_apply {M : Type u} [monoid M] (x : M) (n : multiplicative ) :
((powers_hom M) x) n =
@[simp]
theorem powers_hom_symm_apply {M : Type u} [monoid M] (f : →* M) :
@[simp]
theorem zpowers_hom_apply {G : Type w} [group G] (x : G) (n : multiplicative ) :
((zpowers_hom G) x) n =
@[simp]
theorem zpowers_hom_symm_apply {G : Type w} [group G] (f : →* G) :
@[simp]
theorem multiples_hom_apply {A : Type y} [add_monoid A] (x : A) (n : ) :
( x) n = n x
@[simp]
theorem multiples_hom_symm_apply {A : Type y} [add_monoid A] (f : →+ A) :
@[simp]
theorem zmultiples_hom_apply {A : Type y} [add_group A] (x : A) (n : ) :
( x) n = n x
@[simp]
theorem zmultiples_hom_symm_apply {A : Type y} [add_group A] (f : →+ A) :
theorem monoid_hom.apply_mnat {M : Type u} [monoid M] (f : →* M) (n : multiplicative ) :
f n =
@[ext]
theorem monoid_hom.ext_mnat {M : Type u} [monoid M] ⦃f g : →* M⦄ (h : = ) :
f = g
theorem monoid_hom.apply_mint {M : Type u} [group M] (f : →* M) (n : multiplicative ) :
f n =

`monoid_hom.ext_mint` is defined in `data.int.cast`

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`

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`

def powers_mul_hom (M : Type u) [comm_monoid M] :
M ≃*

If `M` is commutative, `powers_hom` is a multiplicative equivalence.

Equations
def zpowers_mul_hom (G : Type w) [comm_group G] :
G ≃*

If `M` is commutative, `zpowers_hom` is a multiplicative equivalence.

Equations
def multiples_add_hom (A : Type y)  :
A ≃+ ( →+ A)

If `M` is commutative, `multiples_hom` is an additive equivalence.

Equations
def zmultiples_add_hom (A : Type y)  :
A ≃+ ( →+ A)

If `M` is commutative, `zmultiples_hom` is an additive equivalence.

Equations
@[simp]
theorem powers_mul_hom_apply {M : Type u} [comm_monoid M] (x : M) (n : multiplicative ) :
( x) n =
@[simp]
theorem powers_mul_hom_symm_apply {M : Type u} [comm_monoid M] (f : →* M) :
@[simp]
theorem zpowers_mul_hom_apply {G : Type w} [comm_group G] (x : G) (n : multiplicative ) :
( x) n =
@[simp]
theorem zpowers_mul_hom_symm_apply {G : Type w} [comm_group G] (f : →* G) :
@[simp]
theorem multiples_add_hom_apply {A : Type y} (x : A) (n : ) :
( x) n = n x
@[simp]
theorem multiples_add_hom_symm_apply {A : Type y} (f : →+ A) :
.symm) f = f 1
@[simp]
theorem zmultiples_add_hom_apply {A : Type y} (x : A) (n : ) :
( x) n = n x
@[simp]
theorem zmultiples_add_hom_symm_apply {A : Type y} (f : →+ 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.

@[simp]
theorem semiconj_by.cast_nat_mul_right {R : Type u₁} [semiring R] {a x y : R} (h : x y) (n : ) :
(n * x) (n * y)
@[simp]
theorem semiconj_by.cast_nat_mul_left {R : Type u₁} [semiring R] {a x y : R} (h : x y) (n : ) :
semiconj_by (n * a) x y
@[simp]
theorem semiconj_by.cast_nat_mul_cast_nat_mul {R : Type u₁} [semiring R] {a x y : R} (h : x y) (m n : ) :
semiconj_by (m * a) (n * x) (n * y)
@[simp]
theorem add_semiconj_by.add_units_zsmul_right {M : Type u} [add_monoid M] {a : M} {x y : add_units M} (h : y) (m : ) :
(m x) (m y)
@[simp]
theorem semiconj_by.units_zpow_right {M : Type u} [monoid M] {a : M} {x y : Mˣ} (h : x y) (m : ) :
(x ^ m) (y ^ m)
@[simp]
theorem semiconj_by.cast_int_mul_right {R : Type u₁} [ring R] {a x y : R} (h : x y) (m : ) :
(m * x) (m * y)
@[simp]
theorem semiconj_by.cast_int_mul_left {R : Type u₁} [ring R] {a x y : R} (h : x y) (m : ) :
semiconj_by (m * a) x y
@[simp]
theorem semiconj_by.cast_int_mul_cast_int_mul {R : Type u₁} [ring R] {a x y : R} (h : x y) (m n : ) :
semiconj_by (m * a) (n * x) (n * y)
@[simp]
theorem commute.cast_nat_mul_right {R : Type u₁} [semiring R] {a b : R} (h : b) (n : ) :
(n * b)
@[simp]
theorem commute.cast_nat_mul_left {R : Type u₁} [semiring R] {a b : R} (h : b) (n : ) :
commute (n * a) b
@[simp]
theorem commute.cast_nat_mul_cast_nat_mul {R : Type u₁} [semiring R] {a b : R} (h : b) (m n : ) :
commute (m * a) (n * b)
@[simp]
theorem commute.self_cast_nat_mul {R : Type u₁} [semiring R] (a : R) (n : ) :
(n * a)
@[simp]
theorem commute.cast_nat_mul_self {R : Type u₁} [semiring R] (a : R) (n : ) :
commute (n * a) a
@[simp]
theorem commute.self_cast_nat_mul_cast_nat_mul {R : Type u₁} [semiring R] (a : R) (m n : ) :
commute (m * a) (n * a)
@[simp]
theorem commute.units_zpow_right {M : Type u} [monoid M] {a : M} {u : Mˣ} (h : u) (m : ) :
(u ^ m)
@[simp]
(m u)
@[simp]
theorem commute.units_zpow_left {M : Type u} [monoid M] {u : Mˣ} {a : M} (h : a) (m : ) :
commute (u ^ m) a
@[simp]
@[simp]
theorem commute.cast_int_mul_right {R : Type u₁} [ring R] {a b : R} (h : b) (m : ) :
(m * b)
@[simp]
theorem commute.cast_int_mul_left {R : Type u₁} [ring R] {a b : R} (h : b) (m : ) :
commute (m * a) b
theorem commute.cast_int_mul_cast_int_mul {R : Type u₁} [ring R] {a b : R} (h : b) (m n : ) :
commute (m * a) (n * b)
@[simp]
theorem commute.cast_int_left {R : Type u₁} [ring R] (a : R) (m : ) :
a
@[simp]
theorem commute.cast_int_right {R : Type u₁} [ring R] (a : R) (m : ) :
m
@[simp]
theorem commute.self_cast_int_mul {R : Type u₁} [ring R] (a : R) (n : ) :
(n * a)
@[simp]
theorem commute.cast_int_mul_self {R : Type u₁} [ring R] (a : R) (n : ) :
commute (n * a) a
theorem commute.self_cast_int_mul_cast_int_mul {R : Type u₁} [ring R] (a : R) (m n : ) :
commute (m * a) (n * a)
@[simp]
@[simp]
theorem nat.of_add_mul (a b : ) :
@[simp]
@[simp]
@[simp]
theorem int.of_add_mul (a b : ) :
theorem units.conj_pow {M : Type u} [monoid M] (u : Mˣ) (x : M) (n : ) :
(u * x * u⁻¹) ^ n = u * x ^ n * u⁻¹
theorem units.conj_pow' {M : Type u} [monoid M] (u : Mˣ) (x : M) (n : ) :
(u⁻¹ * x * u) ^ n = u⁻¹ * x ^ n * u
@[simp]
theorem mul_opposite.op_pow {M : Type u} [monoid M] (x : M) (n : ) :

Moving to the opposite monoid commutes with taking powers.

@[simp]
theorem mul_opposite.unop_pow {M : Type u} [monoid M] (x : Mᵐᵒᵖ) (n : ) :
@[simp]
theorem mul_opposite.op_zpow {M : Type u} (x : M) (z : ) :

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

@[simp]
theorem mul_opposite.unop_zpow {M : Type u} (x : Mᵐᵒᵖ) (z : ) :