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} [AddMonoidWithOne A] (n : ℕ) : n • 1 = ↑n

instance invertiblePow {M : Type u} [Monoid M] (m : M) [Invertible m] (n : ℕ) : Invertible (m ^ n)

Equations

• invertiblePow m n = { invOf := ⅟m ^ n, invOf_mul_self := (_ : ⅟m ^ n * m ^ n = 1), mul_invOf_self := (_ : m ^ n * ⅟m ^ n = 1) }

theorem invOf_pow {M : Type u} [Monoid M] (m : M) [Invertible m] (n : ℕ) [Invertible (m ^ n)] : ⅟(m ^ n) = ⅟m ^ n

theorem IsAddUnit.nsmul {M : Type u} [AddMonoid M] {m : M} (n : ℕ) : IsAddUnit m → IsAddUnit (n • m)

abbrev IsAddUnit.nsmul.match_1 {M : Type u_1} [AddMonoid M] {m : M} (motive : IsAddUnit m → Prop) : ∀ (x : IsAddUnit m), (∀ (u : AddUnits M) (hu : ↑u = m), motive (_ : ∃ u, ↑u = m)) → motive x

Equations

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

theorem IsUnit.pow {M : Type u} [Monoid M] {m : M} (n : ℕ) : IsUnit m → IsUnit (m ^ n)

def AddUnits.ofNSMul {M : Type u} [AddMonoid M] (u : AddUnits M) (x : M) {n : ℕ} (hn : n ≠ 0) (hu : n • x = ↑u) : AddUnits M

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

Equations

• AddUnits.ofNSMul u x hn hu = AddUnits.leftOfAdd u x ((n - 1) • x) (_ : x + (n - 1) • x = ↑u) (_ : AddCommute x ((n - 1) • x))

theorem AddUnits.ofNSMul.proof_2 {M : Type u_1} [AddMonoid M] (x : M) {n : ℕ} : AddCommute x ((n - 1) • x)

theorem AddUnits.ofNSMul.proof_1 {M : Type u_1} [AddMonoid M] (u : AddUnits M) (x : M) {n : ℕ} (hn : n ≠ 0) (hu : n • x = ↑u) : x + (n - 1) • x = ↑u

def Units.ofPow {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

• Units.ofPow u x hn hu = Units.leftOfMul u x (x ^ (n - 1)) (_ : x * x ^ (n - 1) = ↑u) (_ : Commute x (x ^ (n - 1)))

abbrev isAddUnit_nsmul_iff.match_1 {M : Type u_1} [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

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

@[simp]

theorem isAddUnit_nsmul_iff {M : Type u} [AddMonoid M] {a : M} {n : ℕ} (hn : n ≠ 0) : IsAddUnit (n • a) ↔ IsAddUnit a

@[simp]

theorem isUnit_pow_iff {M : Type u} [Monoid M] {a : M} {n : ℕ} (hn : n ≠ 0) : IsUnit (a ^ n) ↔ IsUnit a

theorem isAddUnit_nsmul_succ_iff {M : Type u} [AddMonoid M] {m : M} {n : ℕ} : IsAddUnit ((n + 1) • m) ↔ IsAddUnit m

theorem isUnit_pow_succ_iff {M : Type u} [Monoid M] {m : M} {n : ℕ} : IsUnit (m ^ (n + 1)) ↔ IsUnit m

def AddUnits.ofNSMulEqZero {M : Type u} [AddMonoid M] (x : M) (n : ℕ) (hx : n • x = 0) (hn : n ≠ 0) : AddUnits M

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

Equations

• AddUnits.ofNSMulEqZero x n hx hn = AddUnits.ofNSMul 0 x hn hx

@[simp]

theorem Units.val_ofPowEqOne {M : Type u} [Monoid M] (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) : ↑(Units.ofPowEqOne x n hx hn) = x

@[simp]

theorem Units.val_inv_ofPowEqOne {M : Type u} [Monoid M] (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) : ↑(Units.ofPowEqOne x n hx hn)⁻¹ = x ^ (n - 1)

@[simp]

theorem AddUnits.val_neg_ofNSMulEqZero {M : Type u} [AddMonoid M] (x : M) (n : ℕ) (hx : n • x = 0) (hn : n ≠ 0) : ↑(-AddUnits.ofNSMulEqZero x n hx hn) = (n - 1) • x

@[simp]

theorem AddUnits.val_ofNSMulEqZero {M : Type u} [AddMonoid M] (x : M) (n : ℕ) (hx : n • x = 0) (hn : n ≠ 0) : ↑(AddUnits.ofNSMulEqZero x n hx hn) = x

def Units.ofPowEqOne {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

• Units.ofPowEqOne x n hx hn = Units.ofPow 1 x hn hx

@[simp]

theorem AddUnits.nsmul_ofNSMulEqZero {M : Type u} [AddMonoid M] {x : M} {n : ℕ} (hx : n • x = 0) (hn : n ≠ 0) : n • AddUnits.ofNSMulEqZero x n hx hn = 0

@[simp]

theorem Units.pow_ofPowEqOne {M : Type u} [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} [AddMonoid M] {x : M} {n : ℕ} (hx : n • x = 0) (hn : n ≠ 0) : IsAddUnit x

theorem isUnit_ofPowEqOne {M : Type u} [Monoid M] {x : M} {n : ℕ} (hx : x ^ n = 1) (hn : n ≠ 0) : IsUnit x

def invertibleOfPowEqOne {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

• invertibleOfPowEqOne x n hx hn = Units.invertible (Units.ofPowEqOne x n hx hn)

theorem smul_pow {M : Type u} {N : Type v} [Monoid M] [Monoid N] [MulAction M N] [IsScalarTower M N N] [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} [Monoid M] [Monoid N] [MulDistribMulAction M N] (x : M) (m : N) (n : ℕ) : x • m ^ n = (x • m) ^ n

@[simp]

theorem zsmul_one {A : Type y} [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

• (_ : 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

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

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

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

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_strictMono_right {α : 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

@[simp]

theorem WithBot.coe_nsmul {A : Type y} [AddMonoid A] (a : A) (n : ℕ) : ↑(n • a) = n • ↑a

theorem nsmul_eq_mul' {R : Type u₁} [NonAssocSemiring R] (a : R) (n : ℕ) : n • a = a * ↑n

@[simp]

theorem nsmul_eq_mul {R : Type u₁} [NonAssocSemiring R] (n : ℕ) (a : R) : n • a = ↑n * a

instance NonUnitalNonAssocSemiring.nat_smulCommClass {R : Type u₁} [NonUnitalNonAssocSemiring R] : SMulCommClass ℕ R R

Note that AddCommMonoid.nat_smulCommClass requires stronger assumptions on R.

Equations

• @NonUnitalNonAssocSemiring.nat_smulCommClass = @NonUnitalNonAssocSemiring.nat_smulCommClass.proof_1

instance NonUnitalNonAssocSemiring.nat_isScalarTower {R : Type u₁} [NonUnitalNonAssocSemiring R] : IsScalarTower ℕ R R

Note that AddCommMonoid.nat_isScalarTower requires stronger assumptions on R.

Equations

• @NonUnitalNonAssocSemiring.nat_isScalarTower = @NonUnitalNonAssocSemiring.nat_isScalarTower.proof_1

@[simp]

theorem Nat.cast_pow {R : Type u₁} [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 : ℕ) : Int.natAbs (n ^ k) = Int.natAbs n ^ k

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

@[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

instance NonUnitalNonAssocRing.int_smulCommClass {R : Type u₁} [NonUnitalNonAssocRing R] : SMulCommClass ℤ R R

Note that AddCommGroup.int_smulCommClass requires stronger assumptions on R.

Equations

• @NonUnitalNonAssocRing.int_smulCommClass = @NonUnitalNonAssocRing.int_smulCommClass.proof_1

instance NonUnitalNonAssocRing.int_isScalarTower {R : Type u₁} [NonUnitalNonAssocRing R] : IsScalarTower ℤ R R

Note that AddCommGroup.int_isScalarTower requires stronger assumptions on R.

Equations

• @NonUnitalNonAssocRing.int_isScalarTower = @NonUnitalNonAssocRing.int_isScalarTower.proof_1

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₁} [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₁} [OrderedSemiring 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).

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 => a ^ bit1 n

theorem one_add_mul_le_pow {R : Type u₁} [LinearOrderedRing R] {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₁} [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.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 x_1 => x ^ x_1) x)

def multiplesHom (A : Type y) [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) [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) [Monoid M] : M ≃ (Multiplicative ℕ →* M)

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

Equations

• powersHom M = Additive.ofMul.trans ((multiplesHom (Additive M)).trans AddMonoidHom.toMultiplicative'')

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 powersHom_apply {M : Type u} [Monoid M] (x : M) (n : Multiplicative ℕ) : ↑(↑(powersHom M) x) n = x ^ ↑Multiplicative.toAdd n

@[simp]

theorem powersHom_symm_apply {M : Type u} [Monoid M] (f : Multiplicative ℕ →* M) : ↑(powersHom M).symm f = ↑f (↑Multiplicative.ofAdd 1)

@[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 multiplesHom_apply {A : Type y} [AddMonoid A] (x : A) (n : ℕ) : ↑(↑(multiplesHom A) x) n = n • x

@[simp]

theorem multiplesHom_symm_apply {A : Type y} [AddMonoid A] (f : ℕ →+ A) : ↑(multiplesHom A).symm f = ↑f 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_mnat {M : Type u} [Monoid M] (f : Multiplicative ℕ →* M) (n : Multiplicative ℕ) : ↑f n = ↑f (↑Multiplicative.ofAdd 1) ^ ↑Multiplicative.toAdd n

theorem MonoidHom.ext_mnat {M : Type u} [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} [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} [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} [AddGroup M] (f : ℤ →+ M) (n : ℤ) : ↑f n = n • ↑f 1

AddMonoidHom.ext_int is defined in Data.Int.Cast

def powersMulHom (M : Type u) [CommMonoid M] : M ≃* (Multiplicative ℕ →* 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) [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 multiplesAddHom (A : Type y) [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) [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} [CommMonoid M] (x : M) (n : Multiplicative ℕ) : ↑(↑(powersMulHom M) x) n = x ^ ↑Multiplicative.toAdd n

@[simp]

theorem powersMulHom_symm_apply {M : Type u} [CommMonoid M] (f : Multiplicative ℕ →* M) : ↑(MulEquiv.symm (powersMulHom M)) f = ↑f (↑Multiplicative.ofAdd 1)

@[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 multiplesAddHom_apply {A : Type y} [AddCommMonoid A] (x : A) (n : ℕ) : ↑(↑(multiplesAddHom A) x) n = n • x

@[simp]

theorem multiplesAddHom_symm_apply {A : Type y} [AddCommMonoid A] (f : ℕ →+ A) : ↑(AddEquiv.symm (multiplesAddHom A)) f = ↑f 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

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₁} [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₁} [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₁} [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} [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} [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₁} [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₁} [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₁} [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₁} [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₁} [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₁} [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₁} [Semiring R] (a : R) (n : ℕ) : Commute a (↑n * a)

theorem Commute.cast_nat_mul_self {R : Type u₁} [Semiring R] (a : R) (n : ℕ) : Commute (↑n * a) a

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 AddCommute.addUnits_zsmul_right {M : Type u} [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} [Monoid M] {a : M} {u : Mˣ} (h : Commute a ↑u) (m : ℤ) : Commute a ↑(u ^ m)

@[simp]

theorem AddCommute.addUnits_zsmul_left {M : Type u} [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} [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₁} [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₁} [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₁} [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₁} [Ring R] (a : R) (m : ℤ) : Commute (↑m) a

@[simp]

theorem Commute.cast_int_right {R : Type u₁} [Ring R] (a : R) (m : ℤ) : Commute a ↑m

theorem Commute.self_cast_int_mul {R : Type u₁} [Ring R] (a : R) (n : ℤ) : Commute a (↑n * a)

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]

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} [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 MulOpposite.op_pow {M : Type u} [Monoid M] (x : M) (n : ℕ) : MulOpposite.op (x ^ n) = MulOpposite.op x ^ n

Moving to the opposite monoid commutes with taking powers.

@[simp]

theorem MulOpposite.unop_pow {M : Type u} [Monoid M] (x : Mᵐᵒᵖ) (n : ℕ) : MulOpposite.unop (x ^ n) = MulOpposite.unop x ^ n

@[simp]

theorem MulOpposite.op_zpow {M : Type u} [DivInvMonoid M] (x : M) (z : ℤ) : MulOpposite.op (x ^ z) = MulOpposite.op x ^ z

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

@[simp]

theorem MulOpposite.unop_zpow {M : Type u} [DivInvMonoid M] (x : Mᵐᵒᵖ) (z : ℤ) : MulOpposite.unop (x ^ z) = MulOpposite.unop x ^ z

@[simp]

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