Semirings and rings #

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

This file gives lemmas about semirings, rings and domains. This is analogous to algebra.group.basic, the difference being that the former is about + and * separately, while the present file is about their interaction.

For the definitions of semirings and rings see algebra.ring.defs.

source

@[simp]

theorem commute.add_right {R : Type x} [distrib R] {a b c : R} :

commute a b → commute a c → commute a (b + c)

source

@[simp]

theorem commute.add_left {R : Type x} [distrib R] {a b c : R} :

commute a c → commute b c → commute (a + b) c

source

theorem commute.bit0_right {R : Type x} [distrib R] {x y : R} (h : commute x y) :

commute x (bit0 y)

source

theorem commute.bit0_left {R : Type x} [distrib R] {x y : R} (h : commute x y) :

commute (bit0 x) y

source

theorem commute.bit1_right {R : Type x} [non_assoc_semiring R] {x y : R} (h : commute x y) :

commute x (bit1 y)

source

theorem commute.bit1_left {R : Type x} [non_assoc_semiring R] {x y : R} (h : commute x y) :

commute (bit1 x) y

source

theorem commute.mul_self_sub_mul_self_eq {R : Type x} [non_unital_non_assoc_ring R] {a b : R} (h : commute a b) :

a * a - b * b = (a + b) * (a - b)

Representation of a difference of two squares of commuting elements as a product.

source

theorem commute.mul_self_sub_mul_self_eq' {R : Type x} [non_unital_non_assoc_ring R] {a b : R} (h : commute a b) :

a * a - b * b = (a - b) * (a + b)

source

theorem commute.mul_self_eq_mul_self_iff {R : Type x} [non_unital_non_assoc_ring R] [no_zero_divisors R] {a b : R} (h : commute a b) :

a * a = b * b ↔ a = b ∨ a = -b

source

theorem commute.neg_right {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :

commute a b → commute a (-b)

source

@[simp]

theorem commute.neg_right_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :

commute a (-b) ↔ commute a b

source

theorem commute.neg_left {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :

commute a b → commute (-a) b

source

@[simp]

theorem commute.neg_left_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :

commute (-a) b ↔ commute a b

source

@[simp]

theorem commute.neg_one_right {R : Type x} [mul_one_class R] [has_distrib_neg R] (a : R) :

commute a (-1)

source

@[simp]

theorem commute.neg_one_left {R : Type x} [mul_one_class R] [has_distrib_neg R] (a : R) :

commute (-1) a

source

@[simp]

theorem commute.sub_right {R : Type x} [non_unital_non_assoc_ring R] {a b c : R} :

commute a b → commute a c → commute a (b - c)

source

@[simp]

theorem commute.sub_left {R : Type x} [non_unital_non_assoc_ring R] {a b c : R} :

commute a c → commute b c → commute (a - b) c

source

theorem mul_self_sub_mul_self {R : Type x} [comm_ring R] (a b : R) :

a * a - b * b = (a + b) * (a - b)

Representation of a difference of two squares in a commutative ring as a product.

source

theorem mul_self_sub_one {R : Type x} [non_assoc_ring R] (a : R) :

a * a - 1 = (a + 1) * (a - 1)

source

theorem mul_self_eq_mul_self_iff {R : Type x} [comm_ring R] [no_zero_divisors R] {a b : R} :

a * a = b * b ↔ a = b ∨ a = -b

source

theorem mul_self_eq_one_iff {R : Type x} [non_assoc_ring R] [no_zero_divisors R] {a : R} :

a * a = 1 ↔ a = 1 ∨ a = -1

source

theorem units.inv_eq_self_iff {R : Type x} [ring R] [no_zero_divisors R] (u : Rˣ) :

u⁻¹ = u ↔ u = 1 ∨ u = -1

In the unit group of an integral domain, a unit is its own inverse iff the unit is one or one's additive inverse.