Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Neil Strickland

! This file was ported from Lean 3 source module algebra.ring.commute
! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Ring.Semiconj
import Mathlib.Algebra.Ring.Units
import Mathlib.Algebra.Group.Commute

/-!
# Semirings and rings

This file gives lemmas about semirings, rings and domains.
This is analogous to `Mathlib.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 `Mathlib.Algebra.Ring.Defs`.

-/

universe u v w x

variable {α: Type uα : Type u: Type (u+1)Type u} {β: Type vβ : Type v: Type (v+1)Type v} {γ: Type wγ : Type w: Type (w+1)Type w} {R: Type xR : Type x: Type (x+1)Type x}

open Function

namespace Commute

@[simp]
theorem add_right: ∀ [inst : Distrib R] {a b c : R}, Commute a b → Commute a c → Commute a (b + c)add_right [Distrib: Type ?u.18 → Type ?u.18Distrib R: Type xR] {a: Ra b: Rb c: Rc : R: Type xR} : Commute: {S : Type ?u.28} → [inst : Mul S] → S → S → PropCommute a: Ra b: Rb → Commute: {S : Type ?u.147} → [inst : Mul S] → S → S → PropCommute a: Ra c: Rc → Commute: {S : Type ?u.161} → [inst : Mul S] → S → S → PropCommute a: Ra (b: Rb + c: Rc) :=
SemiconjBy.add_right: ∀ {R : Type ?u.231} [inst : Distrib R] {a x y x' y' : R},
SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x + x') (y + y')SemiconjBy.add_right
#align commute.add_right Commute.add_rightₓ: ∀ {R : Type x} [inst : Distrib R] {a b c : R}, Commute a b → Commute a c → Commute a (b + c)Commute.add_rightₓ
-- for some reason mathport expected `Semiring` instead of `Distrib`?

@[simp]
theorem add_left: ∀ {R : Type x} [inst : Distrib R] {a b c : R}, Commute a c → Commute b c → Commute (a + b) cadd_left [Distrib: Type ?u.301 → Type ?u.301Distrib R: Type xR] {a: Ra b: Rb c: Rc : R: Type xR} : Commute: {S : Type ?u.311} → [inst : Mul S] → S → S → PropCommute a: Ra c: Rc → Commute: {S : Type ?u.430} → [inst : Mul S] → S → S → PropCommute b: Rb c: Rc → Commute: {S : Type ?u.444} → [inst : Mul S] → S → S → PropCommute (a: Ra + b: Rb) c: Rc :=
SemiconjBy.add_left: ∀ {R : Type ?u.514} [inst : Distrib R] {a b x y : R}, SemiconjBy a x y → SemiconjBy b x y → SemiconjBy (a + b) x ySemiconjBy.add_left
#align commute.add_left Commute.add_leftₓ: ∀ {R : Type x} [inst : Distrib R] {a b c : R}, Commute a c → Commute b c → Commute (a + b) cCommute.add_leftₓ
-- for some reason mathport expected `Semiring` instead of `Distrib`?

section deprecated
set_option linter.deprecated false

@[deprecated]
theorem bit0_right: ∀ {R : Type x} [inst : Distrib R] {x y : R}, Commute x y → Commute x (bit0 y)bit0_right [Distrib: Type ?u.583 → Type ?u.583Distrib R: Type xR] {x: Rx y: Ry : R: Type xR} (h: Commute x yh : Commute: {S : Type ?u.590} → [inst : Mul S] → S → S → PropCommute x: Rx y: Ry) : Commute: {S : Type ?u.709} → [inst : Mul S] → S → S → PropCommute x: Rx (bit0: {α : Type ?u.722} → [inst : Add α] → α → αbit0 y: Ry) :=
h: Commute x yh.add_right: ∀ {R : Type ?u.750} [inst : Distrib R] {a b c : R}, Commute a b → Commute a c → Commute a (b + c)add_right h: Commute x yh
#align commute.bit0_right Commute.bit0_right: ∀ {R : Type x} [inst : Distrib R] {x y : R}, Commute x y → Commute x (bit0 y)Commute.bit0_right

@[deprecated]
theorem bit0_left: ∀ {R : Type x} [inst : Distrib R] {x y : R}, Commute x y → Commute (bit0 x) ybit0_left [Distrib: Type ?u.789 → Type ?u.789Distrib R: Type xR] {x: Rx y: Ry : R: Type xR} (h: Commute x yh : Commute: {S : Type ?u.796} → [inst : Mul S] → S → S → PropCommute x: Rx y: Ry) : Commute: {S : Type ?u.915} → [inst : Mul S] → S → S → PropCommute (bit0: {α : Type ?u.928} → [inst : Add α] → α → αbit0 x: Rx) y: Ry :=
h: Commute x yh.add_left: ∀ {R : Type ?u.956} [inst : Distrib R] {a b c : R}, Commute a c → Commute b c → Commute (a + b) cadd_left h: Commute x yh
#align commute.bit0_left Commute.bit0_left: ∀ {R : Type x} [inst : Distrib R] {x y : R}, Commute x y → Commute (bit0 x) yCommute.bit0_left

@[deprecated]
theorem bit1_right: ∀ {R : Type x} [inst : NonAssocSemiring R] {x y : R}, Commute x y → Commute x (bit1 y)bit1_right [NonAssocSemiring: Type ?u.995 → Type ?u.995NonAssocSemiring R: Type xR] {x: Rx y: Ry : R: Type xR} (h: Commute x yh : Commute: {S : Type ?u.1002} → [inst : Mul S] → S → S → PropCommute x: Rx y: Ry) : Commute: {S : Type ?u.1075} → [inst : Mul S] → S → S → PropCommute x: Rx (bit1: {α : Type ?u.1088} → [inst : One α] → [inst : Add α] → α → αbit1 y: Ry) :=
h: Commute x yh.bit0_right: ∀ {R : Type ?u.1212} [inst : Distrib R] {x y : R}, Commute x y → Commute x (bit0 y)bit0_right.add_right: ∀ {R : Type ?u.1255} [inst : Distrib R] {a b c : R}, Commute a b → Commute a c → Commute a (b + c)add_right (Commute.one_right: ∀ {M : Type ?u.1274} [inst : MulOneClass M] (a : M), Commute a 1Commute.one_right x: Rx)
#align commute.bit1_right Commute.bit1_right: ∀ {R : Type x} [inst : NonAssocSemiring R] {x y : R}, Commute x y → Commute x (bit1 y)Commute.bit1_right

@[deprecated]
theorem bit1_left: ∀ {R : Type x} [inst : NonAssocSemiring R] {x y : R}, Commute x y → Commute (bit1 x) ybit1_left [NonAssocSemiring: Type ?u.1306 → Type ?u.1306NonAssocSemiring R: Type xR] {x: Rx y: Ry : R: Type xR} (h: Commute x yh : Commute: {S : Type ?u.1313} → [inst : Mul S] → S → S → PropCommute x: Rx y: Ry) : Commute: {S : Type ?u.1386} → [inst : Mul S] → S → S → PropCommute (bit1: {α : Type ?u.1399} → [inst : One α] → [inst : Add α] → α → αbit1 x: Rx) y: Ry :=
h: Commute x yh.bit0_left: ∀ {R : Type ?u.1523} [inst : Distrib R] {x y : R}, Commute x y → Commute (bit0 x) ybit0_left.add_left: ∀ {R : Type ?u.1566} [inst : Distrib R] {a b c : R}, Commute a c → Commute b c → Commute (a + b) cadd_left (Commute.one_left: ∀ {M : Type ?u.1585} [inst : MulOneClass M] (a : M), Commute 1 aCommute.one_left y: Ry)
#align commute.bit1_left Commute.bit1_left: ∀ {R : Type x} [inst : NonAssocSemiring R] {x y : R}, Commute x y → Commute (bit1 x) yCommute.bit1_left

end deprecated

/-- Representation of a difference of two squares of commuting elements as a product. -/
theorem mul_self_sub_mul_self_eq: ∀ [inst : NonUnitalNonAssocRing R] {a b : R}, Commute a b → a * a - b * b = (a + b) * (a - b)mul_self_sub_mul_self_eq [NonUnitalNonAssocRing: Type ?u.1617 → Type ?u.1617NonUnitalNonAssocRing R: Type xR] {a: Ra b: Rb : R: Type xR} (h: Commute a bh : Commute: {S : Type ?u.1624} → [inst : Mul S] → S → S → PropCommute a: Ra b: Rb) :
a: Ra * a: Ra - b: Rb * b: Rb = (a: Ra + b: Rb) * (a: Ra - b: Rb) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a + b) * (a - b)rw [α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a + b) * (a - b)add_mul: ∀ {R : Type ?u.2056} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
(a + b) * c = a * c + b * cadd_mul,α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = a * (a - b) + b * (a - b) α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a + b) * (a - b)mul_sub: ∀ {α : Type ?u.2241} [inst : NonUnitalNonAssocRing α] (a b c : α), a * (b - c) = a * b - a * cmul_sub,α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = a * a - a * b + b * (a - b) α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a + b) * (a - b)mul_sub: ∀ {α : Type ?u.2283} [inst : NonUnitalNonAssocRing α] (a b c : α), a * (b - c) = a * b - a * cmul_sub,α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = a * a - a * b + (b * a - b * b) α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a + b) * (a - b)h: Commute a bh.eq: ∀ {S : Type ?u.2308} [inst : Mul S] {a b : S}, Commute a b → a * b = b * aeq,α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = a * a - b * a + (b * a - b * b) α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a + b) * (a - b)sub_add_sub_cancel: ∀ {G : Type ?u.2325} [inst : AddGroup G] (a b c : G), a - b + (b - c) = a - csub_add_sub_cancelα: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = a * a - b * b]Goals accomplished! 🐙
#align commute.mul_self_sub_mul_self_eq Commute.mul_self_sub_mul_self_eq: ∀ {R : Type x} [inst : NonUnitalNonAssocRing R] {a b : R}, Commute a b → a * a - b * b = (a + b) * (a - b)Commute.mul_self_sub_mul_self_eq

theorem mul_self_sub_mul_self_eq': ∀ [inst : NonUnitalNonAssocRing R] {a b : R}, Commute a b → a * a - b * b = (a - b) * (a + b)mul_self_sub_mul_self_eq' [NonUnitalNonAssocRing: Type ?u.2407 → Type ?u.2407NonUnitalNonAssocRing R: Type xR] {a: Ra b: Rb : R: Type xR} (h: Commute a bh : Commute: {S : Type ?u.2414} → [inst : Mul S] → S → S → PropCommute a: Ra b: Rb) :
a: Ra * a: Ra - b: Rb * b: Rb = (a: Ra - b: Rb) * (a: Ra + b: Rb) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a - b) * (a + b)rw [α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a - b) * (a + b)mul_add: ∀ {R : Type ?u.2846} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
a * (b + c) = a * b + a * cmul_add,α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a - b) * a + (a - b) * b α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a - b) * (a + b)sub_mul: ∀ {α : Type ?u.3025} [inst : NonUnitalNonAssocRing α] (a b c : α), (a - b) * c = a * c - b * csub_mul,α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = a * a - b * a + (a - b) * b α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a - b) * (a + b)sub_mul: ∀ {α : Type ?u.3073} [inst : NonUnitalNonAssocRing α] (a b c : α), (a - b) * c = a * c - b * csub_mul,α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = a * a - b * a + (a * b - b * b) α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a - b) * (a + b)h: Commute a bh.eq: ∀ {S : Type ?u.3104} [inst : Mul S] {a b : S}, Commute a b → a * b = b * aeq,α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = a * a - b * a + (b * a - b * b) α: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = (a - b) * (a + b)sub_add_sub_cancel: ∀ {G : Type ?u.3121} [inst : AddGroup G] (a b c : G), a - b + (b - c) = a - csub_add_sub_cancelα: Type uβ: Type vγ: Type wR: Type xinst✝: NonUnitalNonAssocRing Ra, b: Rh: Commute a ba * a - b * b = a * a - b * b]Goals accomplished! 🐙
#align commute.mul_self_sub_mul_self_eq' Commute.mul_self_sub_mul_self_eq': ∀ {R : Type x} [inst : NonUnitalNonAssocRing R] {a b : R}, Commute a b → a * a - b * b = (a - b) * (a + b)Commute.mul_self_sub_mul_self_eq'

theorem mul_self_eq_mul_self_iff: ∀ {R : Type x} [inst : NonUnitalNonAssocRing R] [inst_1 : NoZeroDivisors R] {a b : R},
Commute a b → (a * a = b * b ↔ a = b ∨ a = -b)mul_self_eq_mul_self_iff [NonUnitalNonAssocRing: Type ?u.3203 → Type ?u.3203NonUnitalNonAssocRing R: Type xR] [NoZeroDivisors: (M₀ : Type ?u.3206) → [inst : Mul M₀] → [inst : Zero M₀] → PropNoZeroDivisors R: Type xR] {a: Ra b: Rb : R: Type xR}
(h: Commute a bh : Commute: {S : Type ?u.3388} → [inst : Mul S] → S → S → PropCommute a: Ra b: Rb) : a: Ra * a: Ra = b: Rb * b: Rb ↔ a: Ra = b: Rb ∨ a: Ra = -b: Rb := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba * a = b * b ↔ a = b ∨ a = -brw [α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba * a = b * b ↔ a = b ∨ a = -b← sub_eq_zero: ∀ {G : Type ?u.3583} [inst : AddGroup G] {a b : G}, a - b = 0 ↔ a = bsub_eq_zero,α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba * a - b * b = 0 ↔ a = b ∨ a = -b α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba * a = b * b ↔ a = b ∨ a = -bh: Commute a bh.mul_self_sub_mul_self_eq: ∀ {R : Type ?u.3643} [inst : NonUnitalNonAssocRing R] {a b : R}, Commute a b → a * a - b * b = (a + b) * (a - b)mul_self_sub_mul_self_eq,α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a b(a + b) * (a - b) = 0 ↔ a = b ∨ a = -b α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba * a = b * b ↔ a = b ∨ a = -bmul_eq_zero: ∀ {M₀ : Type ?u.3663} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, a * b = 0 ↔ a = 0 ∨ b = 0mul_eq_zero,α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba * a = b * b ↔ a = b ∨ a = -bor_comm: ∀ {a b : Prop}, a ∨ b ↔ b ∨ aor_comm,α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba - b = 0 ∨ a + b = 0 ↔ a = b ∨ a = -b α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba * a = b * b ↔ a = b ∨ a = -bsub_eq_zero: ∀ {G : Type ?u.3747} [inst : AddGroup G] {a b : G}, a - b = 0 ↔ a = bsub_eq_zero,α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba = b ∨ a + b = 0 ↔ a = b ∨ a = -b
α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba * a = b * b ↔ a = b ∨ a = -badd_eq_zero_iff_eq_neg: ∀ {G : Type ?u.3782} [inst : AddGroup G] {a b : G}, a + b = 0 ↔ a = -badd_eq_zero_iff_eq_negα: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonUnitalNonAssocRing Rinst✝: NoZeroDivisors Ra, b: Rh: Commute a ba = b ∨ a = -b ↔ a = b ∨ a = -b]Goals accomplished! 🐙
#align commute.mul_self_eq_mul_self_iff Commute.mul_self_eq_mul_self_iff: ∀ {R : Type x} [inst : NonUnitalNonAssocRing R] [inst_1 : NoZeroDivisors R] {a b : R},
Commute a b → (a * a = b * b ↔ a = b ∨ a = -b)Commute.mul_self_eq_mul_self_iff

section

variable [Mul: Type ?u.3879 → Type ?u.3879Mul R: Type xR] [HasDistribNeg: (α : Type ?u.4253) → [inst : Mul α] → Type ?u.4253HasDistribNeg R: Type xR] {a: Ra b: Rb : R: Type xR}

theorem neg_right: ∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute a b → Commute a (-b)neg_right : Commute: {S : Type ?u.3900} → [inst : Mul S] → S → S → PropCommute a: Ra b: Rb → Commute: {S : Type ?u.3923} → [inst : Mul S] → S → S → PropCommute a: Ra (-b: Rb) :=
SemiconjBy.neg_right: ∀ {R : Type ?u.4200} [inst : Mul R] [inst_1 : HasDistribNeg R] {a x y : R}, SemiconjBy a x y → SemiconjBy a (-x) (-y)SemiconjBy.neg_right
#align commute.neg_right Commute.neg_right: ∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute a b → Commute a (-b)Commute.neg_right

@[simp]
theorem neg_right_iff: Commute a (-b) ↔ Commute a bneg_right_iff : Commute: {S : Type ?u.4270} → [inst : Mul S] → S → S → PropCommute a: Ra (-b: Rb) ↔ Commute: {S : Type ?u.4544} → [inst : Mul S] → S → S → PropCommute a: Ra b: Rb :=
SemiconjBy.neg_right_iff: ∀ {R : Type ?u.4548} [inst : Mul R] [inst_1 : HasDistribNeg R] {a x y : R}, SemiconjBy a (-x) (-y) ↔ SemiconjBy a x ySemiconjBy.neg_right_iff
#align commute.neg_right_iff Commute.neg_right_iff: ∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute a (-b) ↔ Commute a bCommute.neg_right_iff

theorem neg_left: ∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute a b → Commute (-a) bneg_left : Commute: {S : Type ?u.4644} → [inst : Mul S] → S → S → PropCommute a: Ra b: Rb → Commute: {S : Type ?u.4667} → [inst : Mul S] → S → S → PropCommute (-a: Ra) b: Rb :=
SemiconjBy.neg_left: ∀ {R : Type ?u.4944} [inst : Mul R] [inst_1 : HasDistribNeg R] {a x y : R}, SemiconjBy a x y → SemiconjBy (-a) x ySemiconjBy.neg_left
#align commute.neg_left Commute.neg_left: ∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute a b → Commute (-a) bCommute.neg_left

@[simp]
theorem neg_left_iff: ∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute (-a) b ↔ Commute a bneg_left_iff : Commute: {S : Type ?u.5014} → [inst : Mul S] → S → S → PropCommute (-a: Ra) b: Rb ↔ Commute: {S : Type ?u.5288} → [inst : Mul S] → S → S → PropCommute a: Ra b: Rb :=
SemiconjBy.neg_left_iff: ∀ {R : Type ?u.5292} [inst : Mul R] [inst_1 : HasDistribNeg R] {a x y : R}, SemiconjBy (-a) x y ↔ SemiconjBy a x ySemiconjBy.neg_left_iff
#align commute.neg_left_iff Commute.neg_left_iff: ∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute (-a) b ↔ Commute a bCommute.neg_left_iff

end

section

variable [MulOneClass: Type ?u.6445 → Type ?u.6445MulOneClass R: Type xR] [HasDistribNeg: (α : Type ?u.5370) → [inst : Mul α] → Type ?u.5370HasDistribNeg R: Type xR] {a: Ra : R: Type xR}

-- Porting note: no longer needs to be `@[simp]` since `simp` can prove it.
-- @[simp]
theorem neg_one_right: ∀ (a : R), Commute a (-1)neg_one_right (a: Ra : R: Type xR) : Commute: {S : Type ?u.5747} → [inst : Mul S] → S → S → PropCommute a: Ra (-1: ?m.57621) :=
SemiconjBy.neg_one_right: ∀ {R : Type ?u.6423} [inst : MulOneClass R] [inst_1 : HasDistribNeg R] (a : R), SemiconjBy a (-1) (-1)SemiconjBy.neg_one_right a: Ra
#align commute.neg_one_right Commute.neg_one_right: ∀ {R : Type x} [inst : MulOneClass R] [inst_1 : HasDistribNeg R] (a : R), Commute a (-1)Commute.neg_one_right

-- Porting note: no longer needs to be `@[simp]` since `simp` can prove it.
-- @[simp]
theorem neg_one_left: ∀ (a : R), Commute (-1) aneg_one_left (a: Ra : R: Type xR) : Commute: {S : Type ?u.6632} → [inst : Mul S] → S → S → PropCommute (-1: ?m.66471) a: Ra :=
SemiconjBy.neg_one_left: ∀ {R : Type ?u.7321} [inst : MulOneClass R] [inst_1 : HasDistribNeg R] (x : R), SemiconjBy (-1) x xSemiconjBy.neg_one_left a: Ra
#align commute.neg_one_left Commute.neg_one_left: ∀ {R : Type x} [inst : MulOneClass R] [inst_1 : HasDistribNeg R] (a : R), Commute (-1) aCommute.neg_one_left

end

section

variable [NonUnitalNonAssocRing: Type ?u.7360 → Type ?u.7360NonUnitalNonAssocRing R: Type xR] {a: Ra b: Rb c: Rc : R: Type xR}

@[simp]
theorem sub_right: ∀ {R : Type x} [inst : NonUnitalNonAssocRing R] {a b c : R}, Commute a b → Commute a c → Commute a (b - c)sub_right : Commute: {S : Type ?u.7370} → [inst : Mul S] → S → S → PropCommute a: Ra b: Rb → Commute: {S : Type ?u.7401} → [inst : Mul S] → S → S → PropCommute a: Ra c: Rc → Commute: {S : Type ?u.7415} → [inst : Mul S] → S → S → PropCommute a: Ra (b: Rb - c: Rc) :=
SemiconjBy.sub_right: ∀ {R : Type ?u.7573} [inst : NonUnitalNonAssocRing R] {a x y x' y' : R},
SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x - x') (y - y')SemiconjBy.sub_right
#align commute.sub_right Commute.sub_right: ∀ {R : Type x} [inst : NonUnitalNonAssocRing R] {a b c : R}, Commute a b → Commute a c → Commute a (b - c)Commute.sub_right

@[simp]
theorem sub_left: Commute a c → Commute b c → Commute (a - b) csub_left : Commute: {S : Type ?u.7655} → [inst : Mul S] → S → S → PropCommute a: Ra c: Rc → Commute: {S : Type ?u.7686} → [inst : Mul S] → S → S → PropCommute b: Rb c: Rc → Commute: {S : Type ?u.7700} → [inst : Mul S] → S → S → PropCommute (a: Ra - b: Rb) c: Rc :=
SemiconjBy.sub_left: ∀ {R : Type ?u.7858} [inst : NonUnitalNonAssocRing R] {a b x y : R},
SemiconjBy a x y → SemiconjBy b x y → SemiconjBy (a - b) x ySemiconjBy.sub_left
#align commute.sub_left Commute.sub_left: ∀ {R : Type x} [inst : NonUnitalNonAssocRing R] {a b c : R}, Commute a c → Commute b c → Commute (a - b) cCommute.sub_left

end

end Commute

/-- Representation of a difference of two squares in a commutative ring as a product. -/
theorem mul_self_sub_mul_self: ∀ {R : Type x} [inst : CommRing R] (a b : R), a * a - b * b = (a + b) * (a - b)mul_self_sub_mul_self [CommRing: Type ?u.7929 → Type ?u.7929CommRing R: Type xR] (a: Ra b: Rb : R: Type xR) : a: Ra * a: Ra - b: Rb * b: Rb = (a: Ra + b: Rb) * (a: Ra - b: Rb) :=
(Commute.all: ∀ {S : Type ?u.8262} [inst : CommSemigroup S] (a b : S), Commute a bCommute.all a: Ra b: Rb).mul_self_sub_mul_self_eq: ∀ {R : Type ?u.8278} [inst : NonUnitalNonAssocRing R] {a b : R}, Commute a b → a * a - b * b = (a + b) * (a - b)mul_self_sub_mul_self_eq
#align mul_self_sub_mul_self mul_self_sub_mul_self: ∀ {R : Type x} [inst : CommRing R] (a b : R), a * a - b * b = (a + b) * (a - b)mul_self_sub_mul_self

theorem mul_self_sub_one: ∀ [inst : NonAssocRing R] (a : R), a * a - 1 = (a + 1) * (a - 1)mul_self_sub_one [NonAssocRing: Type ?u.8325 → Type ?u.8325NonAssocRing R: Type xR] (a: Ra : R: Type xR) : a: Ra * a: Ra - 1: ?m.83381 = (a: Ra + 1: ?m.83601) * (a: Ra - 1: ?m.83741) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝: NonAssocRing Ra: Ra * a - 1 = (a + 1) * (a - 1)rw [α: Type uβ: Type vγ: Type wR: Type xinst✝: NonAssocRing Ra: Ra * a - 1 = (a + 1) * (a - 1)← (Commute.one_right: ∀ {M : Type ?u.8733} [inst : MulOneClass M] (a : M), Commute a 1Commute.one_right a: Ra).mul_self_sub_mul_self_eq: ∀ {R : Type ?u.8773} [inst : NonUnitalNonAssocRing R] {a b : R}, Commute a b → a * a - b * b = (a + b) * (a - b)mul_self_sub_mul_self_eq,α: Type uβ: Type vγ: Type wR: Type xinst✝: NonAssocRing Ra: Ra * a - 1 = a * a - 1 * 1 α: Type uβ: Type vγ: Type wR: Type xinst✝: NonAssocRing Ra: Ra * a - 1 = (a + 1) * (a - 1)mul_one: ∀ {M : Type ?u.8821} [inst : MulOneClass M] (a : M), a * 1 = amul_oneα: Type uβ: Type vγ: Type wR: Type xinst✝: NonAssocRing Ra: Ra * a - 1 = a * a - 1]Goals accomplished! 🐙
#align mul_self_sub_one mul_self_sub_one: ∀ {R : Type x} [inst : NonAssocRing R] (a : R), a * a - 1 = (a + 1) * (a - 1)mul_self_sub_one

theorem mul_self_eq_mul_self_iff: ∀ [inst : CommRing R] [inst_1 : NoZeroDivisors R] {a b : R}, a * a = b * b ↔ a = b ∨ a = -bmul_self_eq_mul_self_iff [CommRing: Type ?u.8871 → Type ?u.8871CommRing R: Type xR] [NoZeroDivisors: (M₀ : Type ?u.8874) → [inst : Mul M₀] → [inst : Zero M₀] → PropNoZeroDivisors R: Type xR] {a: Ra b: Rb : R: Type xR} :
a: Ra * a: Ra = b: Rb * b: Rb ↔ a: Ra = b: Rb ∨ a: Ra = -b: Rb :=
(Commute.all: ∀ {S : Type ?u.9079} [inst : CommSemigroup S] (a b : S), Commute a bCommute.all a: Ra b: Rb).mul_self_eq_mul_self_iff: ∀ {R : Type ?u.9095} [inst : NonUnitalNonAssocRing R] [inst_1 : NoZeroDivisors R] {a b : R},
Commute a b → (a * a = b * b ↔ a = b ∨ a = -b)mul_self_eq_mul_self_iff
#align mul_self_eq_mul_self_iff mul_self_eq_mul_self_iff: ∀ {R : Type x} [inst : CommRing R] [inst_1 : NoZeroDivisors R] {a b : R}, a * a = b * b ↔ a = b ∨ a = -bmul_self_eq_mul_self_iff

theorem mul_self_eq_one_iff: ∀ [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] {a : R}, a * a = 1 ↔ a = 1 ∨ a = -1mul_self_eq_one_iff [NonAssocRing: Type ?u.9152 → Type ?u.9152NonAssocRing R: Type xR] [NoZeroDivisors: (M₀ : Type ?u.9155) → [inst : Mul M₀] → [inst : Zero M₀] → PropNoZeroDivisors R: Type xR] {a: Ra : R: Type xR} :
a: Ra * a: Ra = 1: ?m.92791 ↔ a: Ra = 1: ?m.93941 ∨ a: Ra = -1: ?m.94131 := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonAssocRing Rinst✝: NoZeroDivisors Ra: Ra * a = 1 ↔ a = 1 ∨ a = -1rw [α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonAssocRing Rinst✝: NoZeroDivisors Ra: Ra * a = 1 ↔ a = 1 ∨ a = -1← (Commute.one_right: ∀ {M : Type ?u.9467} [inst : MulOneClass M] (a : M), Commute a 1Commute.one_right a: Ra).mul_self_eq_mul_self_iff: ∀ {R : Type ?u.9503} [inst : NonUnitalNonAssocRing R] [inst_1 : NoZeroDivisors R] {a b : R},
Commute a b → (a * a = b * b ↔ a = b ∨ a = -b)mul_self_eq_mul_self_iff,α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonAssocRing Rinst✝: NoZeroDivisors Ra: Ra * a = 1 ↔ a * a = 1 * 1 α: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonAssocRing Rinst✝: NoZeroDivisors Ra: Ra * a = 1 ↔ a = 1 ∨ a = -1mul_one: ∀ {M : Type ?u.9548} [inst : MulOneClass M] (a : M), a * 1 = amul_oneα: Type uβ: Type vγ: Type wR: Type xinst✝¹: NonAssocRing Rinst✝: NoZeroDivisors Ra: Ra * a = 1 ↔ a * a = 1]Goals accomplished! 🐙
#align mul_self_eq_one_iff mul_self_eq_one_iff: ∀ {R : Type x} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] {a : R}, a * a = 1 ↔ a = 1 ∨ a = -1mul_self_eq_one_iff

namespace Units

/-- In the unit group of an integral domain, a unit is its own inverse iff the unit is one or