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

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

• (_ : motive x✝ x) = (_ : motive x✝ x)

theorem mul_zsmul' {α : Type u_1} [SubtractionMonoid α] (a : α) (m : ℤ) (n : ℤ) : (m * n) • a = n • m • a

theorem zpow_mul {α : Type u_1} [DivisionMonoid α] (a : α) (m : ℤ) (n : ℤ) : a ^ (m * n) = (a ^ m) ^ n

theorem mul_zsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (m : ℤ) (n : ℤ) : (m * n) • a = m • n • a

theorem zpow_mul' {α : Type u_1} [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

• (_ : motive x) = (_ : motive x)

theorem bit0_zsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) : bit0 n • a = n • a + n • a

theorem zpow_bit0 {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) : a ^ bit0 n = a ^ n * a ^ n

theorem bit0_zsmul' {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) : bit0 n • a = n • (a + a)

theorem zpow_bit0' {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) : a ^ bit0 n = (a * a) ^ n

@[simp]

theorem zpow_bit0_neg {α : Type u_1} [DivisionMonoid α] [HasDistribNeg α] (x : α) (n : ℤ) : (-x) ^ bit0 n = x ^ bit0 n

theorem add_one_zsmul {G : Type w} [AddGroup G] (a : G) (n : ℤ) : (n + 1) • a = n • a + a

abbrev add_one_zsmul.match_1 (motive : ℤ → Prop) : ∀ (x : ℤ), (∀ (n : ℕ), motive (Int.ofNat n)) → (Unit → motive (Int.negSucc 0)) → (∀ (n : ℕ), motive (Int.negSucc (Nat.succ n))) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem zpow_add_one {G : Type w} [Group G] (a : G) (n : ℤ) : a ^ (n + 1) = a ^ n * a

theorem sub_one_zsmul {G : Type w} [AddGroup 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 add_zsmul {G : Type w} [AddGroup G] (a : G) (m : ℤ) (n : ℤ) : (m + n) • a = m • 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_self {G : Type w} [AddGroup G] (b : G) (m : ℤ) : b + m • b = (m + 1) • b

theorem mul_self_zpow {G : Type w} [Group G] (b : G) (m : ℤ) : b * b ^ m = b ^ (m + 1)

theorem add_self_zsmul {G : Type w} [AddGroup 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} [AddGroup 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} [AddGroup 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} [AddGroup 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 bit1_zsmul {G : Type w} [AddGroup G] (a : G) (n : ℤ) : bit1 n • a = n • a + n • a + a

theorem zpow_bit1 {G : Type w} [Group G] (a : G) (n : ℤ) : a ^ bit1 n = a ^ n * a ^ n * a

theorem zsmul_induction_left {G : Type w} [AddGroup 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 AddSubgroup.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} [AddGroup 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 AddSubgroup.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 Mathlib.Algebra.GroupPower.Order with their friends) because they require facts from Mathlib.Data.Int.Basic.

theorem zsmul_pos {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 < a) {k : ℤ} (hk : 0 < k) : 0 < k • a

theorem one_lt_zpow' {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 < a) {k : ℤ} (hk : 0 < k) : 1 < a ^ k

theorem zsmul_strictMono_left {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 < a) : StrictMono fun (n : ℤ) => n • a

theorem zpow_right_strictMono {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 < a) : StrictMono fun (n : ℤ) => a ^ n

theorem zsmul_mono_left {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 ≤ a) : Monotone fun (n : ℤ) => n • a

theorem zpow_mono_right {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 ≤ a) : Monotone fun (n : ℤ) => a ^ n

theorem zsmul_le_zsmul {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 ≤ a) (h : m ≤ n) : m • a ≤ n • a

theorem zpow_le_zpow {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 ≤ a) (h : m ≤ n) : a ^ m ≤ a ^ n

theorem zsmul_lt_zsmul {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 < a) (h : m < n) : m • a < n • a

theorem zpow_lt_zpow {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 < a) (h : m < n) : a ^ m < a ^ n

theorem zsmul_le_zsmul_iff {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 < a) : m • a ≤ n • a ↔ m ≤ n

theorem zpow_le_zpow_iff {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n

theorem zsmul_lt_zsmul_iff {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 < a) : m • a < n • a ↔ m < n

theorem zpow_lt_zpow_iff {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 < a) : a ^ m < a ^ n ↔ m < n

theorem zsmul_strictMono_right (α : Type u_1) [OrderedAddCommGroup α] {n : ℤ} (hn : 0 < n) : StrictMono fun (x : α) => n • x

theorem zpow_strictMono_left (α : Type u_1) [OrderedCommGroup α] {n : ℤ} (hn : 0 < n) : StrictMono fun (x : α) => x ^ n

theorem zsmul_mono_right (α : Type u_1) [OrderedAddCommGroup α] {n : ℤ} (hn : 0 ≤ n) : Monotone fun (x : α) => n • x

theorem zpow_mono_left (α : Type u_1) [OrderedCommGroup α] {n : ℤ} (hn : 0 ≤ n) : Monotone fun (x : α) => x ^ n

theorem zsmul_le_zsmul' {α : Type u_1} [OrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 ≤ n) (h : a ≤ b) : n • a ≤ n • b

theorem zpow_le_zpow' {α : Type u_1} [OrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 ≤ n) (h : a ≤ b) : a ^ n ≤ b ^ n

theorem zsmul_lt_zsmul' {α : Type u_1} [OrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) (h : a < b) : n • a < n • b

theorem zpow_lt_zpow' {α : Type u_1} [OrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) (h : a < b) : a ^ n < b ^ n

theorem zsmul_le_zsmul_iff' {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} (hn : 0 < n) {a : α} {b : α} : n • a ≤ n • b ↔ a ≤ b

theorem zpow_le_zpow_iff' {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} (hn : 0 < n) {a : α} {b : α} : a ^ n ≤ b ^ n ↔ a ≤ b

theorem zsmul_lt_zsmul_iff' {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} (hn : 0 < n) {a : α} {b : α} : n • a < n • b ↔ a < b

theorem zpow_lt_zpow_iff' {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} (hn : 0 < n) {a : α} {b : α} : a ^ n < b ^ n ↔ a < b

theorem zsmul_right_injective {α : Type u_1} [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} [LinearOrderedCommGroup α] {n : ℤ} (hn : n ≠ 0) : Function.Injective fun (x : α) => x ^ n

theorem zsmul_right_inj {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : n ≠ 0) : n • a = n • b ↔ a = b

theorem zpow_left_inj {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b

theorem zsmul_eq_zsmul_iff' {α : Type u_1} [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} [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} [LinearOrderedAddCommGroup α] (n : ℕ) (a : α) : |n • a| = n • |a|

theorem abs_zsmul {α : Type u_1} [LinearOrderedAddCommGroup α] (n : ℤ) (a : α) : |n • a| = |n| • |a|

theorem abs_add_eq_add_abs_le {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} (hle : a ≤ b) : |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem abs_add_eq_add_abs_iff {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem bit0_mul {R : Type u₁} [NonUnitalNonAssocRing R] {n : R} {r : R} : bit0 n * r = 2 • (n * r)

theorem mul_bit0 {R : Type u₁} [NonUnitalNonAssocRing R] {n : R} {r : R} : r * bit0 n = 2 • (r * n)

theorem bit1_mul {R : Type u₁} [NonAssocRing R] {n : R} {r : R} : bit1 n * r = 2 • (n * r) + r

theorem mul_bit1 {R : Type u₁} [NonAssocRing R] {n : R} {r : R} : r * bit1 n = 2 • (r * n) + r

theorem Int.cast_mul_eq_zsmul_cast {α : Type u_1} [AddCommGroupWithOne α] (m : ℤ) (n : ℤ) : ↑(m * n) = m • ↑n

Note this holds in marginally more generality than Int.cast_mul

theorem neg_one_pow_eq_pow_mod_two {R : Type u₁} [Ring R] {n : ℕ} : (-1) ^ n = (-1) ^ (n % 2)

theorem pow_le_pow_of_le_one_aux {R : Type u₁} [OrderedSemiring 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₁} [OrderedSemiring 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₁} [OrderedSemiring R] {a : R} (h₀ : 0 ≤ a) (h₁ : a ≤ 1) {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ a

theorem sq_le {R : Type u₁} [OrderedSemiring R] {a : R} (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : a ^ 2 ≤ a

theorem sign_cases_of_C_mul_pow_nonneg {R : Type u₁} [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₁} [LinearOrderedRing R] (a : R) (n : ℕ) : |a ^ n| = |a| ^ n

@[simp]

theorem pow_bit1_neg_iff {R : Type u₁} [LinearOrderedRing R] {a : R} {n : ℕ} : a ^ bit1 n < 0 ↔ a < 0

@[simp]

theorem pow_bit1_nonneg_iff {R : Type u₁} [LinearOrderedRing R] {a : R} {n : ℕ} : 0 ≤ a ^ bit1 n ↔ 0 ≤ a

@[simp]

theorem pow_bit1_nonpos_iff {R : Type u₁} [LinearOrderedRing R] {a : R} {n : ℕ} : a ^ bit1 n ≤ 0 ↔ a ≤ 0

@[simp]

theorem pow_bit1_pos_iff {R : Type u₁} [LinearOrderedRing R] {a : R} {n : ℕ} : 0 < a ^ bit1 n ↔ 0 < a

theorem strictMono_pow_bit1 {R : Type u₁} [LinearOrderedRing R] (n : ℕ) : StrictMono fun (a : R) => a ^ bit1 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.natAbs_le_self_sq (a : ℤ) : ↑(Int.natAbs a) ≤ a ^ 2

theorem Int.natAbs_le_self_pow_two (a : ℤ) : ↑(Int.natAbs a) ≤ a ^ 2

Alias of Int.natAbs_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 < Int.natAbs x) : Function.Injective fun (x_1 : ℕ) => x ^ x_1

def zmultiplesHom (A : Type y) [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 zpowersHom (G : Type w) [Group G] : G ≃ (Multiplicative ℤ →* G)

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

Equations

• zpowersHom G = Additive.ofMul.trans ((zmultiplesHom (Additive G)).trans AddMonoidHom.toMultiplicative'')

@[simp]

theorem zpowersHom_apply {G : Type w} [Group G] (x : G) (n : Multiplicative ℤ) : ((zpowersHom G) x) n = x ^ Multiplicative.toAdd n

@[simp]

theorem zpowersHom_symm_apply {G : Type w} [Group G] (f : Multiplicative ℤ →* G) : (zpowersHom G).symm f = f (Multiplicative.ofAdd 1)

@[simp]

theorem zmultiplesHom_apply {A : Type y} [AddGroup A] (x : A) (n : ℤ) : ((zmultiplesHom A) x) n = n • x

@[simp]

theorem zmultiplesHom_symm_apply {A : Type y} [AddGroup A] (f : ℤ →+ A) : (zmultiplesHom A).symm f = f 1

theorem MonoidHom.apply_mint {M : Type u} [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

AddMonoidHom.ext_nat is defined in Data.Nat.Cast

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

AddMonoidHom.ext_int is defined in Data.Int.Cast

def zpowersMulHom (G : Type w) [CommGroup G] : G ≃* (Multiplicative ℤ →* G)

If M is commutative, zpowersHom is a multiplicative equivalence.

Equations

• One or more equations did not get rendered due to their size.

def zmultiplesAddHom (A : Type y) [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 zpowersMulHom_apply {G : Type w} [CommGroup G] (x : G) (n : Multiplicative ℤ) : ((zpowersMulHom G) x) n = x ^ Multiplicative.toAdd n

@[simp]

theorem zpowersMulHom_symm_apply {G : Type w} [CommGroup G] (f : Multiplicative ℤ →* G) : (MulEquiv.symm (zpowersMulHom G)) f = f (Multiplicative.ofAdd 1)

@[simp]

theorem zmultiplesAddHom_apply {A : Type y} [AddCommGroup A] (x : A) (n : ℤ) : ((zmultiplesAddHom A) x) n = n • x

@[simp]

theorem zmultiplesAddHom_symm_apply {A : Type y} [AddCommGroup A] (f : ℤ →+ A) : (AddEquiv.symm (zmultiplesAddHom A)) f = f 1

@[simp]

theorem pow_eq {m : ℤ} {n : ℕ} : Int.pow m n = m ^ n