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 #

source

@[simp]

theorem nsmul_one {A : Type y} [AddMonoidWithOne A] (n : ℕ) :

n • 1 = ↑n

source

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

Invertible (m ^ n)

source

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

⅟(m ^ n) = ⅟m ^ n

source

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

IsAddUnit m → IsAddUnit (n • m)

source

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

Instances For

source

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

IsUnit m → IsUnit (m ^ n)

source

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.

Instances For

source

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

AddCommute x ((n - 1) • x)

source

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

source

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.

Instances For

source

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

Instances For

source

@[simp]

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

IsAddUnit (n • a) ↔ IsAddUnit a

source

@[simp]

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

IsUnit (a ^ n) ↔ IsUnit a

source

theorem isAddUnit_nsmul_succ_iff {M : Type u} [AddMonoid M] {m : M} {n : ℕ} :

IsAddUnit ((n + 1) • m) ↔ IsAddUnit m

source

theorem isUnit_pow_succ_iff {M : Type u} [Monoid M] {m : M} {n : ℕ} :

IsUnit (m ^ (n + 1)) ↔ IsUnit m

source

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.

Instances For

source

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

source

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

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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

IsAddUnit x

source

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

IsUnit x

source

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

Instances For

source

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

source

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

source

@[simp]

theorem zsmul_one {A : Type y} [AddGroupWithOne A] (n : ℤ) :

n • 1 = ↑n

source

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

Instances For

source

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

(m * n) • a = n • m • a

source

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

a ^ (m * n) = (a ^ m) ^ n

source

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

(m * n) • a = m • n • a

source

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

a ^ (m * n) = (a ^ n) ^ m

source

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

bit0 n • a = n • a + n • a

source

abbrev bit0_zsmul.match_1 (motive : ℤ → Prop) :

(x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x

Instances For

source

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

a ^ bit0 n = a ^ n * a ^ n

source

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

bit0 n • a = n • (a + a)

source

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

a ^ bit0 n = (a * a) ^ n

source

@[simp]

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

(-x) ^ bit0 n = x ^ bit0 n

source

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

Instances For

source

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

(n + 1) • a = n • a + a

source

theorem zpow_add_one {G : Type w} [Group G] (a : G) (n : ℤ) :

a ^ (n + 1) = a ^ n * a

source

theorem sub_one_zsmul {G : Type w} [AddGroup G] (a : G) (n : ℤ) :

(n - 1) • a = n • a + -a

source

theorem zpow_sub_one {G : Type w} [Group G] (a : G) (n : ℤ) :

a ^ (n - 1) = a ^ n * a⁻¹

source

theorem add_zsmul {G : Type w} [AddGroup G] (a : G) (m : ℤ) (n : ℤ) :

(m + n) • a = m • a + n • a

source

theorem zpow_add {G : Type w} [Group G] (a : G) (m : ℤ) (n : ℤ) :

a ^ (m + n) = a ^ m * a ^ n

source

theorem add_zsmul_self {G : Type w} [AddGroup G] (b : G) (m : ℤ) :

b + m • b = (m + 1) • b

source

theorem mul_self_zpow {G : Type w} [Group G] (b : G) (m : ℤ) :

b * b ^ m = b ^ (m + 1)

source

theorem add_self_zsmul {G : Type w} [AddGroup G] (b : G) (m : ℤ) :

m • b + b = (m + 1) • b

source

theorem mul_zpow_self {G : Type w} [Group G] (b : G) (m : ℤ) :

b ^ m * b = b ^ (m + 1)

source

theorem sub_zsmul {G : Type w} [AddGroup G] (a : G) (m : ℤ) (n : ℤ) :

(m - n) • a = m • a + -(n • a)

source

theorem zpow_sub {G : Type w} [Group G] (a : G) (m : ℤ) (n : ℤ) :

a ^ (m - n) = a ^ m * (a ^ n)⁻¹

source

theorem one_add_zsmul {G : Type w} [AddGroup G] (a : G) (i : ℤ) :

(1 + i) • a = a + i • a

source

theorem zpow_one_add {G : Type w} [Group G] (a : G) (i : ℤ) :

a ^ (1 + i) = a * a ^ i

source

theorem zsmul_add_comm {G : Type w} [AddGroup G] (a : G) (i : ℤ) (j : ℤ) :

i • a + j • a = j • a + i • a

source

theorem zpow_mul_comm {G : Type w} [Group G] (a : G) (i : ℤ) (j : ℤ) :

a ^ i * a ^ j = a ^ j * a ^ i

source

theorem bit1_zsmul {G : Type w} [AddGroup G] (a : G) (n : ℤ) :

bit1 n • a = n • a + n • a + a

source

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

a ^ bit1 n = a ^ n * a ^ n * a

source

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.

source

theorem zpow_induction_left {G : Type w} [Group G] {g : G} {P : G → Prop} (h_one : P 1) (h_mul : (a : G) → P a → P (g * a)) (h_inv : (a : G) → P a → P (g⁻¹ * a)) (n : ℤ) :

P (g ^ n)

To show a property of all powers of g it suffices to show it is closed under multiplication by g and g⁻¹ on the left. For subgroups generated by more than one element, see Subgroup.closure_induction_left.

source

theorem zsmul_induction_right {G : Type w} [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.

source

theorem zpow_induction_right {G : Type w} [Group G] {g : G} {P : G → Prop} (h_one : P 1) (h_mul : (a : G) → P a → P (a * g)) (h_inv : (a : G) → P a → P (a * g⁻¹)) (n : ℤ) :

P (g ^ n)

To show a property of all powers of g it suffices to show it is closed under multiplication by g and g⁻¹ on the right. For subgroups generated by more than one element, see Subgroup.closure_induction_right.

`zpow`/`zsmul` and an order #

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

source

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

0 < k • a

source

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

1 < a ^ k

source

theorem zsmul_strictMono_left {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 < a) :

StrictMono fun n => n • a

source

theorem zpow_strictMono_right {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 < a) :

StrictMono fun n => a ^ n

source

theorem zsmul_mono_left {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 ≤ a) :

Monotone fun n => n • a

source

theorem zpow_mono_right {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 ≤ a) :

Monotone fun n => a ^ n

source

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

m • a ≤ n • a

source

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

a ^ m ≤ a ^ n

source

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

m • a < n • a

source

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

a ^ m < a ^ n

source

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

m • a ≤ n • a ↔ m ≤ n

source

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

a ^ m ≤ a ^ n ↔ m ≤ n

source

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

m • a < n • a ↔ m < n

source

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

a ^ m < a ^ n ↔ m < n

source

theorem zsmul_strictMono_right (α : Type u_1) [OrderedAddCommGroup α] {n : ℤ} (hn : 0 < n) :

StrictMono fun x => n • x

source

theorem zpow_strictMono_left (α : Type u_1) [OrderedCommGroup α] {n : ℤ} (hn : 0 < n) :

StrictMono fun x => x ^ n

source

theorem zsmul_mono_right (α : Type u_1) [OrderedAddCommGroup α] {n : ℤ} (hn : 0 ≤ n) :

Monotone fun x => n • x

source

theorem zpow_mono_left (α : Type u_1) [OrderedCommGroup α] {n : ℤ} (hn : 0 ≤ n) :

Monotone fun x => x ^ n

source

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

n • a ≤ n • b

source

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

a ^ n ≤ b ^ n

source

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

n • a < n • b

source

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

a ^ n < b ^ n

source

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

n • a ≤ n • b ↔ a ≤ b

source

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

a ^ n ≤ b ^ n ↔ a ≤ b

source

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

n • a < n • b ↔ a < b

source

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

a ^ n < b ^ n ↔ a < b

source

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.

source

theorem zpow_left_injective {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} (hn : n ≠ 0) :

Function.Injective fun x => x ^ n

source

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

n • a = n • b ↔ a = b

source

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

a ^ n = b ^ n ↔ a = b

source

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

source

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

source

theorem abs_nsmul {α : Type u_1} [LinearOrderedAddCommGroup α] (n : ℕ) (a : α) :

|n • a| = n • |a|

source

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

|n • a| = |n| • |a|

source

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

source

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

source

@[simp]

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

↑(n • a) = n • ↑a

source

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

n • a = a * ↑n

source

@[simp]

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

n • a = ↑n * a

source

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

SMulCommClass ℕ R R

Note that AddCommMonoid.nat_smulCommClass requires stronger assumptions on R.

source

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

IsScalarTower ℕ R R

Note that AddCommMonoid.nat_isScalarTower requires stronger assumptions on R.

source

@[simp]

theorem Nat.cast_pow {R : Type u₁} [Semiring R] (n : ℕ) (m : ℕ) :

↑(n ^ m) = ↑n ^ m

source

theorem Int.coe_nat_pow (n : ℕ) (m : ℕ) :

↑(n ^ m) = ↑n ^ m

source

theorem Int.natAbs_pow (n : ℤ) (k : ℕ) :

Int.natAbs (n ^ k) = Int.natAbs n ^ k

source

theorem bit0_mul {R : Type u₁} [NonUnitalNonAssocRing R] {n : R} {r : R} :

bit0 n * r = 2 • (n * r)

source

theorem mul_bit0 {R : Type u₁} [NonUnitalNonAssocRing R] {n : R} {r : R} :

r * bit0 n = 2 • (r * n)

source

theorem bit1_mul {R : Type u₁} [NonAssocRing R] {n : R} {r : R} :

bit1 n * r = 2 • (n * r) + r

source

theorem mul_bit1 {R : Type u₁} [NonAssocRing R] {n : R} {r : R} :

r * bit1 n = 2 • (r * n) + r

source

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

source

@[simp]

theorem zsmul_eq_mul {R : Type u₁} [Ring R] (a : R) (n : ℤ) :

n • a = ↑n * a

source

theorem zsmul_eq_mul' {R : Type u₁} [Ring R] (a : R) (n : ℤ) :

n • a = a * ↑n

source

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

SMulCommClass ℤ R R

Note that AddCommGroup.int_smulCommClass requires stronger assumptions on R.

source

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

IsScalarTower ℤ R R

Note that AddCommGroup.int_isScalarTower requires stronger assumptions on R.

source

theorem zsmul_int_int (a : ℤ) (b : ℤ) :

a • b = a * b

source

theorem zsmul_int_one (n : ℤ) :

n • 1 = n

source

@[simp]

theorem Int.cast_pow {R : Type u₁} [Ring R] (n : ℤ) (m : ℕ) :

↑(n ^ m) = ↑n ^ m

source

theorem neg_one_pow_eq_pow_mod_two {R : Type u₁} [Ring R] {n : ℕ} :

(-1) ^ n = (-1) ^ (n % 2)

source

theorem one_add_mul_le_pow' {R : Type u₁} [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).

source

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

source

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

source

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

source

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

a ^ 2 ≤ a

source

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

source

@[simp]

theorem abs_pow {R : Type u₁} [LinearOrderedRing R] (a : R) (n : ℕ) :

|a ^ n| = |a| ^ n

source

@[simp]

theorem pow_bit1_neg_iff {R : Type u₁} [LinearOrderedRing R] {a : R} {n : ℕ} :

a ^ bit1 n < 0 ↔ a < 0

source

@[simp]

theorem pow_bit1_nonneg_iff {R : Type u₁} [LinearOrderedRing R] {a : R} {n : ℕ} :

0 ≤ a ^ bit1 n ↔ 0 ≤ a

source

@[simp]

theorem pow_bit1_nonpos_iff {R : Type u₁} [LinearOrderedRing R] {a : R} {n : ℕ} :

a ^ bit1 n ≤ 0 ↔ a ≤ 0

source

@[simp]

theorem pow_bit1_pos_iff {R : Type u₁} [LinearOrderedRing R] {a : R} {n : ℕ} :

0 < a ^ bit1 n ↔ 0 < a

source

theorem strictMono_pow_bit1 {R : Type u₁} [LinearOrderedRing R] (n : ℕ) :

StrictMono fun a => a ^ bit1 n

source

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.

source

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.

source

theorem Int.natAbs_sq (x : ℤ) :

↑(Int.natAbs x) ^ 2 = x ^ 2

source

theorem Int.natAbs_pow_two (x : ℤ) :

↑(Int.natAbs x) ^ 2 = x ^ 2

Alias of Int.natAbs_sq.

source

theorem Int.natAbs_le_self_sq (a : ℤ) :

↑(Int.natAbs a) ≤ a ^ 2

source

theorem Int.natAbs_le_self_pow_two (a : ℤ) :

↑(Int.natAbs a) ≤ a ^ 2

Alias of Int.natAbs_le_self_sq.

source

theorem Int.le_self_sq (b : ℤ) :

b ≤ b ^ 2

source

theorem Int.le_self_pow_two (b : ℤ) :

b ≤ b ^ 2

Alias of Int.le_self_sq.

source

theorem Int.pow_right_injective {x : ℤ} (h : 1 < Int.natAbs x) :

Function.Injective ((fun x x_1 => x ^ x_1) x)

source

def multiplesHom (A : Type y) [AddMonoid A] :

A ≃ (ℕ →+ A)

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

Instances For

source

def zmultiplesHom (A : Type y) [AddGroup A] :

A ≃ (ℤ →+ A)

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

Instances For

source

def powersHom (M : Type u) [Monoid M] :

M ≃ (Multiplicative ℕ →* M)

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

Instances For

source

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

G ≃ (Multiplicative ℤ →* G)

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

Instances For

source

@[simp]

theorem powersHom_apply {M : Type u} [Monoid M] (x : M) (n : Multiplicative ℕ) :

↑(↑(powersHom M) x) n = x ^ ↑Multiplicative.toAdd n

source

@[simp]

theorem powersHom_symm_apply {M : Type u} [Monoid M] (f : Multiplicative ℕ →* M) :

↑(powersHom M).symm f = ↑f (↑Multiplicative.ofAdd 1)

source

@[simp]

theorem zpowersHom_apply {G : Type w} [Group G] (x : G) (n : Multiplicative ℤ) :

↑(↑(zpowersHom G) x) n = x ^ ↑Multiplicative.toAdd n

source

@[simp]

theorem zpowersHom_symm_apply {G : Type w} [Group G] (f : Multiplicative ℤ →* G) :

↑(zpowersHom G).symm f = ↑f (↑Multiplicative.ofAdd 1)

source

@[simp]

theorem multiplesHom_apply {A : Type y} [AddMonoid A] (x : A) (n : ℕ) :

↑(↑(multiplesHom A) x) n = n • x

source

@[simp]

theorem multiplesHom_symm_apply {A : Type y} [AddMonoid A] (f : ℕ →+ A) :

↑(multiplesHom A).symm f = ↑f 1

source

@[simp]

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

↑(↑(zmultiplesHom A) x) n = n • x

source

@[simp]

theorem zmultiplesHom_symm_apply {A : Type y} [AddGroup A] (f : ℤ →+ A) :

↑(zmultiplesHom A).symm f = ↑f 1

source

theorem MonoidHom.apply_mnat {M : Type u} [Monoid M] (f : Multiplicative ℕ →* M) (n : Multiplicative ℕ) :

↑f n = ↑f (↑Multiplicative.ofAdd 1) ^ ↑Multiplicative.toAdd n

source

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

source