mathlib documentation

algebra.ring.commute

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.

@[simp]
theorem commute.add_right {R : Type x} [distrib R] {a b c : R} :
commute a b commute a c commute a (b + c)
@[simp]
theorem commute.add_left {R : Type x} [distrib R] {a b c : R} :
commute a c commute b c commute (a + b) c
theorem commute.bit0_right {R : Type x} [distrib R] {x y : R} (h : commute x y) :
theorem commute.bit0_left {R : Type x} [distrib R] {x y : R} (h : commute x y) :
theorem commute.bit1_right {R : Type x} [non_assoc_semiring R] {x y : R} (h : commute x y) :
theorem commute.bit1_left {R : Type x} [non_assoc_semiring R] {x y : R} (h : commute x y) :
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.

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)
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
theorem commute.neg_right {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :
commute a b commute a (-b)
@[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
theorem commute.neg_left {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :
commute a b commute (-a) b
@[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
@[simp]
theorem commute.neg_one_right {R : Type x} [mul_one_class R] [has_distrib_neg R] (a : R) :
commute a (-1)
@[simp]
theorem commute.neg_one_left {R : Type x} [mul_one_class R] [has_distrib_neg R] (a : R) :
commute (-1) a
@[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)
@[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
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.

theorem mul_self_sub_one {R : Type x} [non_assoc_ring R] (a : R) :
a * a - 1 = (a + 1) * (a - 1)
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
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
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.