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

ink

@[simp]

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

n • 1 = ↑n

source

ink

instance invertiblePow {M : Type u} [inst : Monoid M] (m : M) [inst : 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) }

source

ink

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

⅟(m ^ n) = ⅟m ^ n

source

ink

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

IsAddUnit m → IsAddUnit (n • m)

source

ink

abbrev IsAddUnit.nsmul.match_1 {M : Type u_1} [inst : AddMonoid M] {m : M} (motive : IsAddUnit m → Prop) :

(x : IsAddUnit m) → ((u : AddUnits M) → (hu : ↑u = m) → motive (_ : ∃ u, ↑u = m)) → motive x

Equations

IsAddUnit.nsmul.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

source

ink

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

IsUnit m → IsUnit (m ^ n)

source

ink

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

AddCommute x ((n - 1) • x)

Equations

(_ : AddCommute x ((n - 1) • x)) = (_ : AddCommute x ((n - 1) • x))

source

ink

def AddUnits.ofNSMul {M : Type u} [inst : 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))

source

ink

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

(_ : x + (n - 1) • x = ↑u) = (_ : x + (n - 1) • x = ↑u)

source

ink

def Units.ofPow {M : Type u} [inst : 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)))

source

ink

@[simp]

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

IsAddUnit (n • a) ↔ IsAddUnit a

source

ink

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

isAddUnit_nsmul_iff.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

source

ink

@[simp]

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

IsUnit (a ^ n) ↔ IsUnit a

source

ink

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

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

source

ink

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

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

source

ink

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

AddUnits M

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

Equations

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

Mˣ

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

Equations

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

source

ink

@[simp]

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

n • AddUnits.ofNSMulEqZero x n hx hn = 0

source

ink

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

source

ink

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

IsAddUnit x

source

ink

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

IsUnit x

source

ink

def invertibleOfPowEqOne {M : Type u} [inst : 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)

source

ink

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

source

ink

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

source

ink

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

n • 1 = ↑n

source

ink

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.

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

Equations

bit0_zsmul.match_1 motive x h_1 h_2 = Int.casesOn x (fun a => h_1 a) fun a => h_2 a

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

@[simp]

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

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

source

ink

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

add_one_zsmul.match_1 motive x h_1 h_2 h_3 = Int.casesOn x (fun a => h_1 a) fun a => Nat.casesOn a (h_2 ()) fun n => h_3 n

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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.

source

ink

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

0 < k • a

source

ink

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

1 < a ^ k

source

ink

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

StrictMono fun n => n • a

source

ink

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

StrictMono fun n => a ^ n

source

ink

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

Monotone fun n => n • a

source

ink

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

Monotone fun n => a ^ n

source

ink

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

m • a ≤ n • a

source

ink

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

a ^ m ≤ a ^ n

source

ink

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

m • a < n • a

source

ink

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

a ^ m < a ^ n

source

ink

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

m • a ≤ n • a ↔ m ≤ n

source

ink

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

a ^ m ≤ a ^ n ↔ m ≤ n

source

ink

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

m • a < n • a ↔ m < n

source

ink

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

a ^ m < a ^ n ↔ m < n

source

ink

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

StrictMono fun x => n • x

source

ink

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

StrictMono fun x => x ^ n

source

ink

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

Monotone fun x => n • x

source

ink

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

Monotone fun x => x ^ n

source

ink

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

n • a ≤ n • b

source

ink

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

a ^ n ≤ b ^ n

source

ink

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

n • a < n • b

source

ink

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

a ^ n < b ^ n

source

ink

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

n • a ≤ n • b ↔ a ≤ b

source

ink

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

a ^ n ≤ b ^ n ↔ a ≤ b

source

ink

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

n • a < n • b ↔ a < b

source

ink

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

a ^ n < b ^ n ↔ a < b

source

ink

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.

source

ink

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

Function.Injective fun x => x ^ n

source

ink

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

n • a = n • b ↔ a = b

source

ink

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

a ^ n = b ^ n ↔ a = b

source

ink

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

source

ink

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

source

ink

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

abs (n • a) = n • abs a

source

ink

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

abs (n • a) = abs n • abs a

source

ink

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

source

ink

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

source

ink

@[simp]

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

↑(n • a) = n • ↑a

source

ink

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

n • a = a * ↑n

source

ink

@[simp]

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

n • a = ↑n * a

source

ink

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

SMulCommClass ℕ R R

Note that AddCommMonoid.nat_smulCommClass requires stronger assumptions on R.

Equations

@NonUnitalNonAssocSemiring.nat_smulCommClass = @NonUnitalNonAssocSemiring.nat_smulCommClass.proof_1

source

ink

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

IsScalarTower ℕ R R

Note that AddCommMonoid.nat_isScalarTower requires stronger assumptions on R.

Equations

@NonUnitalNonAssocSemiring.nat_isScalarTower = @NonUnitalNonAssocSemiring.nat_isScalarTower.proof_1

source

ink

@[simp]

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

↑(n ^ m) = ↑n ^ m

source

ink

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

↑(n ^ m) = ↑n ^ m

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

@[simp]

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

n • a = ↑n * a

source

ink

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

n • a = a * ↑n

source

ink

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

SMulCommClass ℤ R R

Note that AddCommGroup.int_smulCommClass requires stronger assumptions on R.

Equations

@NonUnitalNonAssocRing.int_smulCommClass = @NonUnitalNonAssocRing.int_smulCommClass.proof_1

source

ink

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

IsScalarTower ℤ R R

Note that AddCommGroup.int_isScalarTower requires stronger assumptions on R.

Equations

@NonUnitalNonAssocRing.int_isScalarTower = @NonUnitalNonAssocRing.int_isScalarTower.proof_1

source

ink

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

a • b = a * b

source

ink

theorem zsmul_int_one (n : ℤ) :

n • 1 = n

source

ink

@[simp]

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

↑(n ^ m) = ↑n ^ m

source

ink

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

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

a ^ 2 ≤ a

source

ink

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

source

ink

@[simp]

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

abs (a ^ n) = abs a ^ n

source

ink

@[simp]

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

a ^ bit1 n < 0 ↔ a < 0

source

ink

@[simp]

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

0 ≤ a ^ bit1 n ↔ 0 ≤ a

source

ink

@[simp]

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

a ^ bit1 n ≤ 0 ↔ a ≤ 0

source

ink

@[simp]

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

0 < a ^ bit1 n ↔ 0 < a

source

ink

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

StrictMono fun a => a ^ bit1 n

source

ink

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.

source

ink

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.

source

ink

theorem Int.natAbs_sq (x : ℤ) :

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

source

ink

theorem Int.natAbs_pow_two (x : ℤ) :

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

Alias of Int.natAbs_sq.

source

ink

theorem Int.natAbs_le_self_sq (a : ℤ) :

↑(Int.natAbs a) ≤ a ^ 2

source

ink

theorem Int.natAbs_le_self_pow_two (a : ℤ) :

↑(Int.natAbs a) ≤ a ^ 2

Alias of Int.natAbs_le_self_sq.

source

ink

theorem Int.le_self_sq (b : ℤ) :

b ≤ b ^ 2

source

ink

theorem Int.le_self_pow_two (b : ℤ) :

b ≤ b ^ 2

Alias of Int.le_self_sq.

source

ink

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

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

source

ink

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.

source

ink

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.

source

ink

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

M ≃ (Multiplicative ℕ →* M)

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

Equations

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

source

ink

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

G ≃ (Multiplicative ℤ →* G)

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

Equations

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

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

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

source

ink

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

source

ink