Documentation

Mathlib.Algebra.GroupPower.Lemmas

Lemmas about power operations on monoids and groups #

This file contains lemmas about Monoid.pow, Group.pow, nsmul, and zsmul which require additional imports besides those available in Mathlib.Algebra.GroupPower.Basic.

(Additive) monoid #

@[simp]
theorem nsmul_one {A : Type y} [inst : AddMonoidWithOne A] (n : ) :
n 1 = n
instance invertiblePow {M : Type u} [inst : Monoid M] (m : M) [inst : Invertible m] (n : ) :
Equations
theorem invOf_pow {M : Type u} [inst : Monoid M] (m : M) [inst : Invertible m] (n : ) [inst : Invertible (m ^ n)] :
(m ^ n) = m ^ n
theorem IsAddUnit.nsmul {M : Type u} [inst : AddMonoid M] {m : M} (n : ) :
IsAddUnit mIsAddUnit (n m)
abbrev IsAddUnit.nsmul.match_1 {M : Type u_1} [inst : AddMonoid M] {m : M} (motive : IsAddUnit mProp) :
(x : IsAddUnit m) → ((u : AddUnits M) → (hu : u = m) → motive (_ : u, u = m)) → motive x
Equations
theorem IsUnit.pow {M : Type u} [inst : Monoid M] {m : M} (n : ) :
IsUnit mIsUnit (m ^ n)
def AddUnits.ofNSMul.proof_2 {M : Type u_1} [inst : AddMonoid M] (x : M) {n : } :
AddCommute x ((n - 1) x)
Equations
def AddUnits.ofNSMul {M : Type u} [inst : AddMonoid M] (u : AddUnits 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 AddUnits.ofNSMul.proof_1 {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (x : M) {n : } (hn : n 0) (hu : n x = u) :
x + (n - 1) x = u
Equations
def Units.ofPow {M : Type u} [inst : 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 isAddUnit_nsmul_iff {M : Type u} [inst : AddMonoid M] {a : M} {n : } (hn : n 0) :
abbrev isAddUnit_nsmul_iff.match_1 {M : Type u_1} [inst : AddMonoid M] {a : M} {n : } (motive : IsAddUnit (n a)Prop) :
(x : IsAddUnit (n a)) → ((u : AddUnits M) → (hu : u = n a) → motive (_ : u, u = n a)) → motive x
Equations
@[simp]
theorem isUnit_pow_iff {M : Type u} [inst : Monoid M] {a : M} {n : } (hn : n 0) :
IsUnit (a ^ n) IsUnit a
theorem isAddUnit_nsmul_succ_iff {M : Type u} [inst : AddMonoid M] {m : M} {n : } :
theorem isUnit_pow_succ_iff {M : Type u} [inst : Monoid M] {m : M} {n : } :
IsUnit (m ^ (n + 1)) IsUnit m
def AddUnits.ofNSMulEqZero {M : Type u} [inst : AddMonoid M] (x : M) (n : ) (hx : n x = 0) (hn : n 0) :

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

Equations
@[simp]
theorem Units.ofPowEqOne_val {M : Type u} [inst : Monoid M] (x : M) (n : ) (hx : x ^ n = 1) (hn : n 0) :
↑(Units.ofPowEqOne x n hx hn) = x
@[simp]
theorem AddUnits.ofNSMulEqZero_val {M : Type u} [inst : AddMonoid M] (x : M) (n : ) (hx : n x = 0) (hn : n 0) :
↑(AddUnits.ofNSMulEqZero x n hx hn) = x
@[simp]
theorem Units.ofPowEqOne_inv {M : Type u} [inst : Monoid M] (x : M) (n : ) (hx : x ^ n = 1) (hn : n 0) :
(Units.ofPowEqOne x n hx hn).inv = x ^ (n - 1)
@[simp]
theorem AddUnits.ofNSMulEqZero_neg {M : Type u} [inst : AddMonoid M] (x : M) (n : ) (hx : n x = 0) (hn : n 0) :
(AddUnits.ofNSMulEqZero x n hx hn).neg = (n - 1) x
def Units.ofPowEqOne {M : Type u} [inst : Monoid M] (x : M) (n : ) (hx : x ^ n = 1) (hn : n 0) :

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

Equations
@[simp]
theorem AddUnits.nsmul_ofNSMulEqZero {M : Type u} [inst : AddMonoid M] {x : M} {n : } (hx : n x = 0) (hn : n 0) :
@[simp]
theorem Units.pow_ofPowEqOne {M : Type u} [inst : Monoid M] {x : M} {n : } (hx : x ^ n = 1) (hn : n 0) :
Units.ofPowEqOne x n hx hn ^ n = 1
theorem isAddUnit_ofNSMulEqZero {M : Type u} [inst : AddMonoid M] {x : M} {n : } (hx : n x = 0) (hn : n 0) :
theorem isUnit_ofPowEqOne {M : Type u} [inst : Monoid M] {x : M} {n : } (hx : x ^ n = 1) (hn : n 0) :
def invertibleOfPowEqOne {M : Type u} [inst : 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} [inst : Monoid M] [inst : Monoid N] [inst : MulAction M N] [inst : IsScalarTower M N N] [inst : SMulCommClass M N N] (k : M) (x : N) (p : ) :
(k x) ^ p = k ^ p x ^ p
@[simp]
theorem smul_pow' {M : Type u} {N : Type v} [inst : Monoid M] [inst : Monoid N] [inst : MulDistribMulAction M N] (x : M) (m : N) (n : ) :
x m ^ n = (x m) ^ n
theorem zsmul_one {A : Type y} [inst : AddGroupWithOne A] (n : ) :
n 1 = n
abbrev mul_zsmul'.match_1 (motive : Prop) :
(x x_1 : ) → ((m n : ) → motive (Int.ofNat m) (Int.ofNat n)) → ((m n : ) → motive (Int.ofNat m) (Int.negSucc n)) → ((m n : ) → motive (Int.negSucc m) (Int.ofNat n)) → ((m n : ) → motive (Int.negSucc m) (Int.negSucc n)) → motive x x_1
Equations
  • One or more equations did not get rendered due to their size.
theorem mul_zsmul' {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (m : ) (n : ) :
(m * n) a = n m a
theorem zpow_mul {α : Type u_1} [inst : DivisionMonoid α] (a : α) (m : ) (n : ) :
a ^ (m * n) = (a ^ m) ^ n
theorem mul_zsmul {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (m : ) (n : ) :
(m * n) a = m n a
theorem zpow_mul' {α : Type u_1} [inst : DivisionMonoid α] (a : α) (m : ) (n : ) :
a ^ (m * n) = (a ^ n) ^ m
abbrev bit0_zsmul.match_1 (motive : Prop) :
(x : ) → ((n : ) → motive (Int.ofNat n)) → ((n : ) → motive (Int.negSucc n)) → motive x
Equations
theorem bit0_zsmul {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ) :
bit0 n a = n a + n a
theorem zpow_bit0 {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ) :
a ^ bit0 n = a ^ n * a ^ n
theorem bit0_zsmul' {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ) :
bit0 n a = n (a + a)
theorem zpow_bit0' {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ) :
a ^ bit0 n = (a * a) ^ n
@[simp]
theorem zpow_bit0_neg {α : Type u_1} [inst : DivisionMonoid α] [inst : HasDistribNeg α] (x : α) (n : ) :
(-x) ^ bit0 n = x ^ bit0 n
abbrev add_one_zsmul.match_1 (motive : Prop) :
(x : ) → ((n : ) → motive (Int.ofNat n)) → (Unitmotive (Int.negSucc 0)) → ((n : ) → motive (Int.negSucc (Nat.succ n))) → motive x
Equations
theorem add_one_zsmul {G : Type w} [inst : AddGroup G] (a : G) (n : ) :
(n + 1) a = n a + a
theorem zpow_add_one {G : Type w} [inst : Group G] (a : G) (n : ) :
a ^ (n + 1) = a ^ n * a
theorem sub_one_zsmul {G : Type w} [inst : AddGroup G] (a : G) (n : ) :
(n - 1) a = n a + -a
theorem zpow_sub_one {G : Type w} [inst : Group G] (a : G) (n : ) :
a ^ (n - 1) = a ^ n * a⁻¹
theorem add_zsmul {G : Type w} [inst : AddGroup G] (a : G) (m : ) (n : ) :
(m + n) a = m a + n a
theorem zpow_add {G : Type w} [inst : Group G] (a : G) (m : ) (n : ) :
a ^ (m + n) = a ^ m * a ^ n
theorem add_zsmul_self {G : Type w} [inst : AddGroup G] (b : G) (m : ) :
b + m b = (m + 1) b
theorem mul_self_zpow {G : Type w} [inst : Group G] (b : G) (m : ) :
b * b ^ m = b ^ (m + 1)
theorem add_self_zsmul {G : Type w} [inst : AddGroup G] (b : G) (m : ) :
m b + b = (m + 1) b
theorem mul_zpow_self {G : Type w} [inst : Group G] (b : G) (m : ) :
b ^ m * b = b ^ (m + 1)
theorem sub_zsmul {G : Type w} [inst : AddGroup G] (a : G) (m : ) (n : ) :
(m - n) a = m a + -(n a)
theorem zpow_sub {G : Type w} [inst : Group G] (a : G) (m : ) (n : ) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
theorem one_add_zsmul {G : Type w} [inst : AddGroup G] (a : G) (i : ) :
(1 + i) a = a + i a
theorem zpow_one_add {G : Type w} [inst : Group G] (a : G) (i : ) :
a ^ (1 + i) = a * a ^ i
theorem zsmul_add_comm {G : Type w} [inst : AddGroup G] (a : G) (i : ) (j : ) :
i a + j a = j a + i a
theorem zpow_mul_comm {G : Type w} [inst : Group G] (a : G) (i : ) (j : ) :
a ^ i * a ^ j = a ^ j * a ^ i
theorem bit1_zsmul {G : Type w} [inst : AddGroup G] (a : G) (n : ) :
bit1 n a = n a + n a + a
theorem zpow_bit1 {G : Type w} [inst : Group G] (a : G) (n : ) :
a ^ bit1 n = a ^ n * a ^ n * a

zpow/zsmul and an order #

Those lemmas are placed here (rather than in Mathlib.Algebra.GroupPower.Order with their friends) because they require facts from Mathlib.Data.Int.Basic.

theorem zsmul_pos {α : Type u_1} [inst : OrderedAddCommGroup α] {a : α} (ha : 0 < a) {k : } (hk : 0 < k) :
0 < k a
theorem one_lt_zpow' {α : Type u_1} [inst : OrderedCommGroup α] {a : α} (ha : 1 < a) {k : } (hk : 0 < k) :
1 < a ^ k
theorem zsmul_strictMono_left {α : Type u_1} [inst : OrderedAddCommGroup α] {a : α} (ha : 0 < a) :
StrictMono fun n => n a
theorem zpow_strictMono_right {α : Type u_1} [inst : OrderedCommGroup α] {a : α} (ha : 1 < a) :
StrictMono fun n => a ^ n
theorem zsmul_mono_left {α : Type u_1} [inst : OrderedAddCommGroup α] {a : α} (ha : 0 a) :
Monotone fun n => n a
theorem zpow_mono_right {α : Type u_1} [inst : OrderedCommGroup α] {a : α} (ha : 1 a) :
Monotone fun n => a ^ n
theorem zsmul_le_zsmul {α : Type u_1} [inst : OrderedAddCommGroup α] {m : } {n : } {a : α} (ha : 0 a) (h : m n) :
m a n a
theorem zpow_le_zpow {α : Type u_1} [inst : OrderedCommGroup α] {m : } {n : } {a : α} (ha : 1 a) (h : m n) :
a ^ m a ^ n
theorem zsmul_lt_zsmul {α : Type u_1} [inst : OrderedAddCommGroup α] {m : } {n : } {a : α} (ha : 0 < a) (h : m < n) :
m a < n a
theorem zpow_lt_zpow {α : Type u_1} [inst : OrderedCommGroup α] {m : } {n : } {a : α} (ha : 1 < a) (h : m < n) :
a ^ m < a ^ n
theorem zsmul_le_zsmul_iff {α : Type u_1} [inst : OrderedAddCommGroup α] {m : } {n : } {a : α} (ha : 0 < a) :
m a n a m n
theorem zpow_le_zpow_iff {α : Type u_1} [inst : OrderedCommGroup α] {m : } {n : } {a : α} (ha : 1 < a) :
a ^ m a ^ n m n
theorem zsmul_lt_zsmul_iff {α : Type u_1} [inst : OrderedAddCommGroup α] {m : } {n : } {a : α} (ha : 0 < a) :
m a < n a m < n
theorem zpow_lt_zpow_iff {α : Type u_1} [inst : OrderedCommGroup α] {m : } {n : } {a : α} (ha : 1 < a) :
a ^ m < a ^ n m < n
theorem zsmul_strictMono_right (α : Type u_1) [inst : OrderedAddCommGroup α] {n : } (hn : 0 < n) :
StrictMono fun x => n x
theorem zpow_strictMono_left (α : Type u_1) [inst : OrderedCommGroup α] {n : } (hn : 0 < n) :
StrictMono fun x => x ^ n
theorem zsmul_mono_right (α : Type u_1) [inst : OrderedAddCommGroup α] {n : } (hn : 0 n) :
Monotone fun x => n x
theorem zpow_mono_left (α : Type u_1) [inst : OrderedCommGroup α] {n : } (hn : 0 n) :
Monotone fun x => x ^ n
theorem zsmul_le_zsmul' {α : Type u_1} [inst : OrderedAddCommGroup α] {n : } {a : α} {b : α} (hn : 0 n) (h : a b) :
n a n b
theorem zpow_le_zpow' {α : Type u_1} [inst : OrderedCommGroup α] {n : } {a : α} {b : α} (hn : 0 n) (h : a b) :
a ^ n b ^ n
theorem zsmul_lt_zsmul' {α : Type u_1} [inst : OrderedAddCommGroup α] {n : } {a : α} {b : α} (hn : 0 < n) (h : a < b) :
n a < n b
theorem zpow_lt_zpow' {α : Type u_1} [inst : OrderedCommGroup α] {n : } {a : α} {b : α} (hn : 0 < n) (h : a < b) :
a ^ n < b ^ n
theorem zsmul_le_zsmul_iff' {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {n : } (hn : 0 < n) {a : α} {b : α} :
n a n b a b
theorem zpow_le_zpow_iff' {α : Type u_1} [inst : LinearOrderedCommGroup α] {n : } (hn : 0 < n) {a : α} {b : α} :
a ^ n b ^ n a b
theorem zsmul_lt_zsmul_iff' {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {n : } (hn : 0 < n) {a : α} {b : α} :
n a < n b a < b
theorem zpow_lt_zpow_iff' {α : Type u_1} [inst : LinearOrderedCommGroup α] {n : } (hn : 0 < n) {a : α} {b : α} :
a ^ n < b ^ n a < b
theorem zsmul_right_injective {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {n : } (hn : n 0) :
Function.Injective fun x => n x

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

theorem zpow_left_injective {α : Type u_1} [inst : LinearOrderedCommGroup α] {n : } (hn : n 0) :
Function.Injective fun x => x ^ n
theorem zsmul_right_inj {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {n : } {a : α} {b : α} (hn : n 0) :
n a = n b a = b
theorem zpow_left_inj {α : Type u_1} [inst : LinearOrderedCommGroup α] {n : } {a : α} {b : α} (hn : n 0) :
a ^ n = b ^ n a = b
theorem zsmul_eq_zsmul_iff' {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {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 zpow_eq_zpow_iff' {α : Type u_1} [inst : LinearOrderedCommGroup α] {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 abs_nsmul {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (n : ) (a : α) :
abs (n a) = n abs a
theorem abs_zsmul {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (n : ) (a : α) :
abs (n a) = abs n abs a
theorem abs_add_eq_add_abs_le {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} (hle : a b) :
abs (a + b) = abs a + abs b 0 a 0 b a 0 b 0
theorem abs_add_eq_add_abs_iff {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :
abs (a + b) = abs a + abs b 0 a 0 b a 0 b 0
@[simp]
theorem WithBot.coe_nsmul {A : Type y} [inst : AddMonoid A] (a : A) (n : ) :
↑(n a) = n a
theorem nsmul_eq_mul' {R : Type u₁} [inst : NonAssocSemiring R] (a : R) (n : ) :
n a = a * n
@[simp]
theorem nsmul_eq_mul {R : Type u₁} [inst : NonAssocSemiring R] (n : ) (a : R) :
n a = n * a
@[simp]
theorem Nat.cast_pow {R : Type u₁} [inst : Semiring R] (n : ) (m : ) :
↑(n ^ m) = n ^ m
theorem Int.coe_nat_pow (n : ) (m : ) :
↑(n ^ m) = n ^ m
theorem Int.natAbs_pow (n : ) (k : ) :
theorem bit0_mul {R : Type u₁} [inst : NonUnitalNonAssocRing R] {n : R} {r : R} :
bit0 n * r = 2 (n * r)
theorem mul_bit0 {R : Type u₁} [inst : NonUnitalNonAssocRing R] {n : R} {r : R} :
r * bit0 n = 2 (r * n)
theorem bit1_mul {R : Type u₁} [inst : NonAssocRing R] {n : R} {r : R} :
bit1 n * r = 2 (n * r) + r
theorem mul_bit1 {R : Type u₁} [inst : NonAssocRing R] {n : R} {r : R} :
r * bit1 n = 2 (r * n) + r
@[simp]
theorem zsmul_eq_mul {R : Type u₁} [inst : Ring R] (a : R) (n : ) :
n a = n * a
theorem zsmul_eq_mul' {R : Type u₁} [inst : Ring R] (a : R) (n : ) :
n a = a * n
theorem zsmul_int_int (a : ) (b : ) :
a b = a * b
theorem zsmul_int_one (n : ) :
n 1 = n
@[simp]
theorem Int.cast_pow {R : Type u₁} [inst : Ring R] (n : ) (m : ) :
↑(n ^ m) = n ^ m
theorem neg_one_pow_eq_pow_mod_two {R : Type u₁} [inst : Ring R] {n : } :
(-1) ^ n = (-1) ^ (n % 2)
theorem one_add_mul_le_pow' {R : Type u₁} [inst : StrictOrderedSemiring 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≤ a * a and 0 ≤ (1 + a) * (1 + a)≤ (1 + a) * (1 + a).

theorem pow_le_pow_of_le_one_aux {R : Type u₁} [inst : StrictOrderedSemiring R] {a : R} (h : 0 a) (ha : a 1) (i : ) (k : ) :
a ^ (i + k) a ^ i
theorem pow_le_pow_of_le_one {R : Type u₁} [inst : StrictOrderedSemiring R] {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₁} [inst : StrictOrderedSemiring R] {a : R} (h₀ : 0 a) (h₁ : a 1) {n : } (hn : n 0) :
a ^ n a
theorem sq_le {R : Type u₁} [inst : StrictOrderedSemiring R] {a : R} (h₀ : 0 a) (h₁ : a 1) :
a ^ 2 a
theorem sign_cases_of_C_mul_pow_nonneg {R : Type u₁} [inst : LinearOrderedSemiring R] {C : R} {r : R} (h : ∀ (n : ), 0 C * r ^ n) :
C = 0 0 < C 0 r
@[simp]
theorem abs_pow {R : Type u₁} [inst : LinearOrderedRing R] (a : R) (n : ) :
abs (a ^ n) = abs a ^ n
@[simp]
theorem pow_bit1_neg_iff {R : Type u₁} [inst : LinearOrderedRing R] {a : R} {n : } :
a ^ bit1 n < 0 a < 0
@[simp]
theorem pow_bit1_nonneg_iff {R : Type u₁} [inst : LinearOrderedRing R] {a : R} {n : } :
0 a ^ bit1 n 0 a
@[simp]
theorem pow_bit1_nonpos_iff {R : Type u₁} [inst : LinearOrderedRing R] {a : R} {n : } :
a ^ bit1 n 0 a 0
@[simp]
theorem pow_bit1_pos_iff {R : Type u₁} [inst : LinearOrderedRing R] {a : R} {n : } :
0 < a ^ bit1 n 0 < a
theorem strictMono_pow_bit1 {R : Type u₁} [inst : LinearOrderedRing R] (n : ) :
StrictMono fun a => a ^ bit1 n
theorem one_add_mul_le_pow {R : Type u₁} [inst : LinearOrderedRing R] {a : R} (H : -2 a) (n : ) :
1 + n * a (1 + a) ^ n

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

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

Bernoulli's inequality reformulated to estimate a^n.

theorem Int.natAbs_sq (x : ) :
↑(Int.natAbs x ^ 2) = x ^ 2
theorem Int.natAbs_pow_two (x : ) :
↑(Int.natAbs x ^ 2) = x ^ 2

Alias of Int.natAbs_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 < Int.natAbs x) :
Function.Injective ((fun x x_1 => x ^ x_1) x)
def multiplesHom (A : Type y) [inst : AddMonoid A] :
A ( →+ A)

Additive homomorphisms from are defined by the image of 1.

Equations
  • One or more equations did not get rendered due to their size.
def zmultiplesHom (A : Type y) [inst : AddGroup A] :
A ( →+ A)

Additive homomorphisms from are defined by the image of 1.

Equations
  • One or more equations did not get rendered due to their size.
def powersHom (M : Type u) [inst : Monoid M] :

Monoid homomorphisms from Multiplicative ℕ are defined by the image of Multiplicative.ofAdd 1.

Equations
def zpowersHom (G : Type w) [inst : Group G] :

Monoid homomorphisms from Multiplicative ℤ are defined by the image of Multiplicative.ofAdd 1.

Equations
@[simp]
theorem powersHom_apply {M : Type u} [inst : Monoid M] (x : M) (n : Multiplicative ) :
↑(↑(powersHom M) x) n = x ^ Multiplicative.toAdd n
@[simp]
theorem powersHom_symm_apply {M : Type u} [inst : Monoid M] (f : Multiplicative →* M) :
↑(Equiv.symm (powersHom M)) f = f (Multiplicative.ofAdd 1)
@[simp]
theorem zpowersHom_apply {G : Type w} [inst : Group G] (x : G) (n : Multiplicative ) :
↑(↑(zpowersHom G) x) n = x ^ Multiplicative.toAdd n
@[simp]
theorem zpowersHom_symm_apply {G : Type w} [inst : Group G] (f : Multiplicative →* G) :
↑(Equiv.symm (zpowersHom G)) f = f (Multiplicative.ofAdd 1)
@[simp]
theorem multiplesHom_apply {A : Type y} [inst : AddMonoid A] (x : A) (n : ) :
↑(↑(multiplesHom A) x) n = n x
@[simp]
theorem multiplesHom_symm_apply {A : Type y} [inst : AddMonoid A] (f : →+ A) :
↑(Equiv.symm (multiplesHom A)) f = f 1
@[simp]
theorem zmultiplesHom_apply {A : Type y} [inst : AddGroup A] (x : A) (n : ) :
↑(↑(zmultiplesHom A) x) n = n x
@[simp]
theorem zmultiplesHom_symm_apply {A : Type y} [inst : AddGroup A] (f : →+ A) :
↑(Equiv.symm (zmultiplesHom A)) f = f 1
theorem MonoidHom.apply_mnat {M : Type u} [inst : Monoid M] (f : Multiplicative →* M) (n : Multiplicative ) :
f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n
theorem MonoidHom.ext_mnat {M : Type u} [inst : Monoid M] ⦃f : Multiplicative →* M ⦃g : Multiplicative →* M (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) :
f = g
theorem MonoidHom.apply_mint {M : Type u} [inst : Group M] (f : Multiplicative →* M) (n : Multiplicative ) :
f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n

MonoidHom.ext_mint is defined in Data.Int.Cast

theorem AddMonoidHom.apply_nat {M : Type u} [inst : AddMonoid M] (f : →+ M) (n : ) :
f n = n f 1

AddMonoidHom.ext_nat is defined in Data.Nat.Cast

theorem AddMonoidHom.apply_int {M : Type u} [inst : AddGroup M] (f : →+ M) (n : ) :
f n = n f 1

AddMonoidHom.ext_int is defined in Data.Int.Cast

def powersMulHom (M : Type u) [inst : CommMonoid M] :

If M is commutative, powersHom is a multiplicative equivalence.

Equations
  • One or more equations did not get rendered due to their size.
def zpowersMulHom (G : Type w) [inst : CommGroup G] :

If M is commutative, zpowersHom is a multiplicative equivalence.

Equations
  • One or more equations did not get rendered due to their size.
def multiplesAddHom (A : Type y) [inst : AddCommMonoid A] :
A ≃+ ( →+ A)

If M is commutative, multiplesHom is an additive equivalence.

Equations
  • One or more equations did not get rendered due to their size.
def zmultiplesAddHom (A : Type y) [inst : AddCommGroup A] :
A ≃+ ( →+ A)

If M is commutative, zmultiplesHom is an additive equivalence.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem powersMulHom_apply {M : Type u} [inst : CommMonoid M] (x : M) (n : Multiplicative ) :
↑(↑(powersMulHom M) x) n = x ^ Multiplicative.toAdd n
@[simp]
theorem powersMulHom_symm_apply {M : Type u} [inst : CommMonoid M] (f : Multiplicative →* M) :
↑(MulEquiv.symm (powersMulHom M)) f = f (Multiplicative.ofAdd 1)
@[simp]
theorem zpowersMulHom_apply {G : Type w} [inst : CommGroup G] (x : G) (n : Multiplicative ) :
↑(↑(zpowersMulHom G) x) n = x ^ Multiplicative.toAdd n
@[simp]
theorem zpowersMulHom_symm_apply {G : Type w} [inst : CommGroup G] (f : Multiplicative →* G) :
↑(MulEquiv.symm (zpowersMulHom G)) f = f (Multiplicative.ofAdd 1)
@[simp]
theorem multiplesAddHom_apply {A : Type y} [inst : AddCommMonoid A] (x : A) (n : ) :
↑(↑(multiplesAddHom A) x) n = n x
@[simp]
theorem multiplesAddHom_symm_apply {A : Type y} [inst : AddCommMonoid A] (f : →+ A) :
↑(AddEquiv.symm (multiplesAddHom A)) f = f 1
@[simp]
theorem zmultiplesAddHom_apply {A : Type y} [inst : AddCommGroup A] (x : A) (n : ) :
↑(↑(zmultiplesAddHom A) x) n = n x
@[simp]
theorem zmultiplesAddHom_symm_apply {A : Type y} [inst : AddCommGroup A] (f : →+ A) :
↑(AddEquiv.symm (zmultiplesAddHom A)) f = f 1

Commutativity (again) #

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

@[simp]
theorem SemiconjBy.cast_nat_mul_right {R : Type u₁} [inst : Semiring R] {a : R} {x : R} {y : R} (h : SemiconjBy a x y) (n : ) :
SemiconjBy a (n * x) (n * y)
@[simp]
theorem SemiconjBy.cast_nat_mul_left {R : Type u₁} [inst : Semiring R] {a : R} {x : R} {y : R} (h : SemiconjBy a x y) (n : ) :
SemiconjBy (n * a) x y
@[simp]
theorem SemiconjBy.cast_nat_mul_cast_nat_mul {R : Type u₁} [inst : Semiring R] {a : R} {x : R} {y : R} (h : SemiconjBy a x y) (m : ) (n : ) :
SemiconjBy (m * a) (n * x) (n * y)
@[simp]
theorem AddSemiconjBy.addUnits_zsmul_right {M : Type u} [inst : AddMonoid M] {a : M} {x : AddUnits M} {y : AddUnits M} (h : AddSemiconjBy a x y) (m : ) :
AddSemiconjBy a ↑(m x) ↑(m y)
@[simp]
theorem SemiconjBy.units_zpow_right {M : Type u} [inst : Monoid M] {a : M} {x : Mˣ} {y : Mˣ} (h : SemiconjBy a x y) (m : ) :
SemiconjBy a ↑(x ^ m) ↑(y ^ m)
@[simp]
theorem SemiconjBy.cast_int_mul_right {R : Type u₁} [inst : Ring R] {a : R} {x : R} {y : R} (h : SemiconjBy a x y) (m : ) :
SemiconjBy a (m * x) (m * y)
@[simp]
theorem SemiconjBy.cast_int_mul_left {R : Type u₁} [inst : Ring R] {a : R} {x : R} {y : R} (h : SemiconjBy a x y) (m : ) :
SemiconjBy (m * a) x y
@[simp]
theorem SemiconjBy.cast_int_mul_cast_int_mul {R : Type u₁} [inst : Ring R] {a : R} {x : R} {y : R} (h : SemiconjBy a x y) (m : ) (n : ) :
SemiconjBy (m * a) (n * x) (n * y)
@[simp]
theorem Commute.cast_nat_mul_right {R : Type u₁} [inst : Semiring R] {a : R} {b : R} (h : Commute a b) (n : ) :
Commute a (n * b)
@[simp]
theorem Commute.cast_nat_mul_left {R : Type u₁} [inst : Semiring R] {a : R} {b : R} (h : Commute a b) (n : ) :
Commute (n * a) b
@[simp]
theorem Commute.cast_nat_mul_cast_nat_mul {R : Type u₁} [inst : Semiring R] {a : R} {b : R} (h : Commute a b) (m : ) (n : ) :
Commute (m * a) (n * b)
theorem Commute.self_cast_nat_mul {R : Type u₁} [inst : Semiring R] {a : R} (n : ) :
Commute a (n * a)
theorem Commute.cast_nat_mul_self {R : Type u₁} [inst : Semiring R] {a : R} (n : ) :
Commute (n * a) a
theorem Commute.self_cast_nat_mul_cast_nat_mul {R : Type u₁} [inst : Semiring R] {a : R} (m : ) (n : ) :
Commute (m * a) (n * a)
@[simp]
theorem AddCommute.addUnits_zsmul_right {M : Type u} [inst : AddMonoid M] {a : M} {u : AddUnits M} (h : AddCommute a u) (m : ) :
AddCommute a ↑(m u)
@[simp]
theorem Commute.units_zpow_right {M : Type u} [inst : Monoid M] {a : M} {u : Mˣ} (h : Commute a u) (m : ) :
Commute a ↑(u ^ m)
@[simp]
theorem AddCommute.addUnits_zsmul_left {M : Type u} [inst : AddMonoid M] {u : AddUnits M} {a : M} (h : AddCommute (u) a) (m : ) :
AddCommute (↑(m u)) a
@[simp]
theorem Commute.units_zpow_left {M : Type u} [inst : Monoid M] {u : Mˣ} {a : M} (h : Commute (u) a) (m : ) :
Commute (↑(u ^ m)) a
@[simp]
theorem Commute.cast_int_mul_right {R : Type u₁} [inst : Ring R] {a : R} {b : R} (h : Commute a b) (m : ) :
Commute a (m * b)
@[simp]
theorem Commute.cast_int_mul_left {R : Type u₁} [inst : Ring R] {a : R} {b : R} (h : Commute a b) (m : ) :
Commute (m * a) b
theorem Commute.cast_int_mul_cast_int_mul {R : Type u₁} [inst : Ring R] {a : R} {b : R} (h : Commute a b) (m : ) (n : ) :
Commute (m * a) (n * b)
@[simp]
theorem Commute.cast_int_left {R : Type u₁} [inst : Ring R] (a : R) (m : ) :
Commute (m) a
@[simp]
theorem Commute.cast_int_right {R : Type u₁} [inst : Ring R] (a : R) (m : ) :
Commute a m
theorem Commute.self_cast_int_mul {R : Type u₁} [inst : Ring R] (a : R) (n : ) :
Commute a (n * a)
theorem Commute.cast_int_mul_self {R : Type u₁} [inst : Ring R] (a : R) (n : ) :
Commute (n * a) a
theorem Commute.self_cast_int_mul_cast_int_mul {R : Type u₁} [inst : Ring R] (a : R) (m : ) (n : ) :
Commute (m * a) (n * a)
@[simp]
theorem Nat.toAdd_pow (a : Multiplicative ) (b : ) :
Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b
@[simp]
theorem Nat.ofAdd_mul (a : ) (b : ) :
Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b
@[simp]
theorem Int.toAdd_pow (a : Multiplicative ) (b : ) :
Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b
@[simp]
theorem Int.toAdd_zpow (a : Multiplicative ) (b : ) :
Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b
@[simp]
theorem Int.ofAdd_mul (a : ) (b : ) :
Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b
theorem Units.conj_pow {M : Type u} [inst : Monoid M] (u : Mˣ) (x : M) (n : ) :
(u * x * u⁻¹) ^ n = u * x ^ n * u⁻¹
theorem Units.conj_pow' {M : Type u} [inst : Monoid M] (u : Mˣ) (x : M) (n : ) :
(u⁻¹ * x * u) ^ n = u⁻¹ * x ^ n * u
@[simp]
theorem MulOpposite.op_pow {M : Type u} [inst : Monoid M] (x : M) (n : ) :
{ unop := x ^ n } = { unop := x } ^ n

Moving to the opposite monoid commutes with taking powers.

@[simp]
theorem MulOpposite.unop_pow {M : Type u} [inst : Monoid M] (x : Mᵐᵒᵖ) (n : ) :
(x ^ n).unop = x.unop ^ n
@[simp]
theorem MulOpposite.op_zpow {M : Type u} [inst : DivInvMonoid M] (x : M) (z : ) :
{ unop := x ^ z } = { unop := x } ^ z

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

@[simp]
theorem MulOpposite.unop_zpow {M : Type u} [inst : DivInvMonoid M] (x : Mᵐᵒᵖ) (z : ) :
(x ^ z).unop = x.unop ^ z
@[simp]
theorem pow_eq {m : } {n : } :
Int.pow m n = m ^ n