mathlib3 documentation

algebra.group_power.ring

Power operations on monoids with zero, semirings, and rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides additional lemmas about the natural power operator on rings and semirings. Further lemmas about ordered semirings and rings can be found in algebra.group_power.lemmas.

source
theorem zero_pow {M : Type u_3} [monoid_with_zero M] {n : ℕ} :
0 < n → 0 ^ n = 0
source
@[simp]
theorem zero_pow' {M : Type u_3} [monoid_with_zero M] (n : ℕ) :
n ≠ 0 → 0 ^ n = 0
source
theorem zero_pow_eq {M : Type u_3} [monoid_with_zero M] (n : ℕ) :
0 ^ n = ite (n = 0) 1 0
source
theorem pow_eq_zero_of_le {M : Type u_3} [monoid_with_zero M] {x : M} {n m : ℕ} (hn : n ≤ m) (hx : x ^ n = 0) :
x ^ m = 0
source
theorem pow_eq_zero {M : Type u_3} [monoid_with_zero M] [no_zero_divisors M] {x : M} {n : ℕ} (H : x ^ n = 0) :
x = 0
source
@[simp]
theorem pow_eq_zero_iff {M : Type u_3} [monoid_with_zero M] [no_zero_divisors M] {a : M} {n : ℕ} (hn : 0 < n) :
a ^ n = 0 ↔ a = 0
source
theorem pow_eq_zero_iff' {M : Type u_3} [monoid_with_zero M] [no_zero_divisors M] [nontrivial M] {a : M} {n : ℕ} :
a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
source
theorem pow_ne_zero_iff {M : Type u_3} [monoid_with_zero M] [no_zero_divisors M] {a : M} {n : ℕ} (hn : 0 < n) :
a ^ n ≠ 0 ↔ a ≠ 0
source
theorem ne_zero_pow {M : Type u_3} [monoid_with_zero M] {a : M} {n : ℕ} (hn : n ≠ 0) :
a ^ n ≠ 0 → a ≠ 0
source
theorem pow_ne_zero {M : Type u_3} [monoid_with_zero M] [no_zero_divisors M] {a : M} (n : ℕ) (h : a ≠ 0) :
a ^ n ≠ 0
source
@[protected, instance]
def ne_zero.pow {M : Type u_3} [monoid_with_zero M] [no_zero_divisors M] {x : M} [ne_zero x] {n : ℕ} :
ne_zero (x ^ n)
source
theorem sq_eq_zero_iff {M : Type u_3} [monoid_with_zero M] [no_zero_divisors M] {a : M} :
a ^ 2 = 0 ↔ a = 0
source
@[simp]
theorem zero_pow_eq_zero {M : Type u_3} [monoid_with_zero M] [nontrivial M] {n : ℕ} :
0 ^ n = 0 ↔ 0 < n
source
theorem ring.inverse_pow {M : Type u_3} [monoid_with_zero M] (r : M) (n : ℕ) :
ring.inverse r ^ n = ring.inverse (r ^ n)
source
def pow_monoid_with_zero_hom {M : Type u_3} [comm_monoid_with_zero M] {n : ℕ} (hn : 0 < n) :
M →*₀ M

We define x ↦ x^n (for positive n : ℕ) as a monoid_with_zero_hom

Equations
source
@[simp]
theorem coe_pow_monoid_with_zero_hom {M : Type u_3} [comm_monoid_with_zero M] {n : ℕ} (hn : 0 < n) :
⇑(pow_monoid_with_zero_hom hn) = λ (_x : M), _x ^ n
source
@[simp]
theorem pow_monoid_with_zero_hom_apply {M : Type u_3} [comm_monoid_with_zero M] {n : ℕ} (hn : 0 < n) (a : M) :
⇑(pow_monoid_with_zero_hom hn) a = a ^ n
source
theorem pow_dvd_pow_iff {R : Type u_1} [cancel_comm_monoid_with_zero R] {x : R} {n m : ℕ} (h0 : x ≠ 0) (h1 : ¬is_unit x) :
x ^ n ∣ x ^ m ↔ n ≤ m
source
@[protected]
theorem ring_hom.map_pow {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R →+* S) (a : R) (n : ℕ) :
⇑f (a ^ n) = ⇑f a ^ n
source
theorem min_pow_dvd_add {R : Type u_1} [semiring R] {n m : ℕ} {a b c : R} (ha : c ^ n ∣ a) (hb : c ^ m ∣ b) :
c ^ linear_order.min n m ∣ a + b
source
theorem add_sq {R : Type u_1} [comm_semiring R] (a b : R) :
(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
source
theorem add_sq' {R : Type u_1} [comm_semiring R] (a b : R) :
(a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b
source
theorem add_pow_two {R : Type u_1} [comm_semiring R] (a b : R) :
(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

Alias of add_sq.

source
theorem neg_one_pow_eq_or (R : Type u_1) [monoid R] [has_distrib_neg R] (n : ℕ) :
(-1) ^ n = 1 ∨ (-1) ^ n = -1
source
theorem neg_pow {R : Type u_1} [monoid R] [has_distrib_neg R] (a : R) (n : ℕ) :
(-a) ^ n = (-1) ^ n * a ^ n
source
@[simp]
theorem neg_pow_bit0 {R : Type u_1} [monoid R] [has_distrib_neg R] (a : R) (n : ℕ) :
(-a) ^ bit0 n = a ^ bit0 n
source
@[simp]
theorem neg_pow_bit1 {R : Type u_1} [monoid R] [has_distrib_neg R] (a : R) (n : ℕ) :
(-a) ^ bit1 n = -a ^ bit1 n
source
@[simp]
theorem neg_sq {R : Type u_1} [monoid R] [has_distrib_neg R] (a : R) :
(-a) ^ 2 = a ^ 2
source
@[simp]
theorem neg_one_sq {R : Type u_1} [monoid R] [has_distrib_neg R] :
(-1) ^ 2 = 1
source
theorem neg_pow_two {R : Type u_1} [monoid R] [has_distrib_neg R] (a : R) :
(-a) ^ 2 = a ^ 2

Alias of neg_sq.

source
theorem neg_one_pow_two {R : Type u_1} [monoid R] [has_distrib_neg R] :
(-1) ^ 2 = 1

Alias of neg_one_sq.

source
@[protected]
theorem commute.sq_sub_sq {R : Type u_1} [ring R] {a b : R} (h : commute a b) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)
source
@[simp]
theorem neg_one_pow_mul_eq_zero_iff {R : Type u_1} [ring R] {n : ℕ} {r : R} :
(-1) ^ n * r = 0 ↔ r = 0
source
@[simp]
theorem mul_neg_one_pow_eq_zero_iff {R : Type u_1} [ring R] {n : ℕ} {r : R} :
r * (-1) ^ n = 0 ↔ r = 0
source
@[protected]
theorem commute.sq_eq_sq_iff_eq_or_eq_neg {R : Type u_1} [ring R] {a b : R} [no_zero_divisors R] (h : commute a b) :
a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
source
@[simp]
theorem sq_eq_one_iff {R : Type u_1} [ring R] {a : R} [no_zero_divisors R] :
a ^ 2 = 1 ↔ a = 1 ∨ a = -1
source
theorem sq_ne_one_iff {R : Type u_1} [ring R] {a : R} [no_zero_divisors R] :
a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1
source
theorem sq_sub_sq {R : Type u_1} [comm_ring R] (a b : R) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)
source
theorem pow_two_sub_pow_two {R : Type u_1} [comm_ring R] (a b : R) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)

Alias of sq_sub_sq.

source
theorem sub_sq {R : Type u_1} [comm_ring R] (a b : R) :
(a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
source
theorem sub_pow_two {R : Type u_1} [comm_ring R] (a b : R) :
(a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Alias of sub_sq.

source
theorem sub_sq' {R : Type u_1} [comm_ring R] (a b : R) :
(a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b
source
theorem sq_eq_sq_iff_eq_or_eq_neg {R : Type u_1} [comm_ring R] [no_zero_divisors R] {a b : R} :
a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
source
theorem eq_or_eq_neg_of_sq_eq_sq {R : Type u_1} [comm_ring R] [no_zero_divisors R] (a b : R) :
a ^ 2 = b ^ 2 → a = b ∨ a = -b
source
@[protected]
theorem units.sq_eq_sq_iff_eq_or_eq_neg {R : Type u_1} [comm_ring R] [no_zero_divisors R] {a b : Rˣ} :
a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
source
@[protected]
theorem units.eq_or_eq_neg_of_sq_eq_sq {R : Type u_1} [comm_ring R] [no_zero_divisors R] (a b : Rˣ) (h : a ^ 2 = b ^ 2) :
a = b ∨ a = -b