mathlib3documentation

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} :
b c (b + c)
@[simp]
theorem commute.add_left {R : Type x} [distrib R] {a b c : R} :
c c commute (a + b) c
theorem commute.bit0_right {R : Type x} [distrib R] {x y : R} (h : y) :
(bit0 y)
theorem commute.bit0_left {R : Type x} [distrib R] {x y : R} (h : y) :
theorem commute.bit1_right {R : Type x} {x y : R} (h : y) :
(bit1 y)
theorem commute.bit1_left {R : Type x} {x y : R} (h : y) :
theorem commute.mul_self_sub_mul_self_eq {R : Type x} {a b : R} (h : 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} {a b : R} (h : b) :
a * a - b * b = (a - b) * (a + b)
theorem commute.mul_self_eq_mul_self_iff {R : Type x} {a b : R} (h : b) :
a * a = b * b a = b a = -b
theorem commute.neg_right {R : Type x} [has_mul R] {a b : R} :
b (-b)
@[simp]
theorem commute.neg_right_iff {R : Type x} [has_mul R] {a b : R} :
(-b) b
theorem commute.neg_left {R : Type x} [has_mul R] {a b : R} :
b commute (-a) b
@[simp]
theorem commute.neg_left_iff {R : Type x} [has_mul R] {a b : R} :
commute (-a) b b
@[simp]
theorem commute.neg_one_right {R : Type x} (a : R) :
(-1)
@[simp]
theorem commute.neg_one_left {R : Type x} (a : R) :
commute (-1) a
@[simp]
theorem commute.sub_right {R : Type x} {a b c : R} :
b c (b - c)
@[simp]
theorem commute.sub_left {R : Type x} {a b c : R} :
c 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} (a : R) :
a * a - 1 = (a + 1) * (a - 1)
theorem mul_self_eq_mul_self_iff {R : Type x} [comm_ring R] {a b : R} :
a * a = b * b a = b a = -b
theorem mul_self_eq_one_iff {R : Type x} {a : R} :
a * a = 1 a = 1 a = -1
theorem units.inv_eq_self_iff {R : Type x} [ring 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.