/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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 x
R : 
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.18
Distrib 
R: Type x
R] {
a: R
a 
b: R
b 
c: R
c : 
R: Type x
R} : 
Commute: {S : Type ?u.28} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a 
b: R
b → 
Commute: {S : Type ?u.147} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a 
c: R
c → 
Commute: {S : Type ?u.161} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a (
b: R
b + 
c: R
c) :=
  
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) c
add_left [
Distrib: Type ?u.301 → Type ?u.301
Distrib 
R: Type x
R] {
a: R
a 
b: R
b 
c: R
c : 
R: Type x
R} : 
Commute: {S : Type ?u.311} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a 
c: R
c → 
Commute: {S : Type ?u.430} → [inst : Mul S] → S → S → Prop
Commute 
b: R
b 
c: R
c → 
Commute: {S : Type ?u.444} → [inst : Mul S] → S → S → Prop
Commute (
a: R
a + 
b: R
b) 
c: R
c :=
  
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 y
SemiconjBy.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) c
Commute.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.583
Distrib 
R: Type x
R] {
x: R
x 
y: R
y : 
R: Type x
R} (
h: Commute x y
h : 
Commute: {S : Type ?u.590} → [inst : Mul S] → S → S → Prop
Commute 
x: R
x 
y: R
y) : 
Commute: {S : Type ?u.709} → [inst : Mul S] → S → S → Prop
Commute 
x: R
x (
bit0: {α : Type ?u.722} → [inst : Add α] → α → α
bit0 
y: R
y) :=
  
h: Commute x y
h.
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 y
h
#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) y
bit0_left [
Distrib: Type ?u.789 → Type ?u.789
Distrib 
R: Type x
R] {
x: R
x 
y: R
y : 
R: Type x
R} (
h: Commute x y
h : 
Commute: {S : Type ?u.796} → [inst : Mul S] → S → S → Prop
Commute 
x: R
x 
y: R
y) : 
Commute: {S : Type ?u.915} → [inst : Mul S] → S → S → Prop
Commute (
bit0: {α : Type ?u.928} → [inst : Add α] → α → α
bit0 
x: R
x) 
y: R
y :=
  
h: Commute x y
h.
add_left: ∀ {R : Type ?u.956} [inst : Distrib R] {a b c : R}, Commute a c → Commute b c → Commute (a + b) c
add_left 
h: Commute x y
h
#align commute.bit0_left 
Commute.bit0_left: ∀ {R : Type x} [inst : Distrib R] {x y : R}, Commute x y → Commute (bit0 x) y
Commute.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.995
NonAssocSemiring 
R: Type x
R] {
x: R
x 
y: R
y : 
R: Type x
R} (
h: Commute x y
h : 
Commute: {S : Type ?u.1002} → [inst : Mul S] → S → S → Prop
Commute 
x: R
x 
y: R
y) : 
Commute: {S : Type ?u.1075} → [inst : Mul S] → S → S → Prop
Commute 
x: R
x (
bit1: {α : Type ?u.1088} → [inst : One α] → [inst : Add α] → α → α
bit1 
y: R
y) :=
  
h: Commute x y
h.
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 1
Commute.one_right 
x: R
x)
#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) y
bit1_left [
NonAssocSemiring: Type ?u.1306 → Type ?u.1306
NonAssocSemiring 
R: Type x
R] {
x: R
x 
y: R
y : 
R: Type x
R} (
h: Commute x y
h : 
Commute: {S : Type ?u.1313} → [inst : Mul S] → S → S → Prop
Commute 
x: R
x 
y: R
y) : 
Commute: {S : Type ?u.1386} → [inst : Mul S] → S → S → Prop
Commute (
bit1: {α : Type ?u.1399} → [inst : One α] → [inst : Add α] → α → α
bit1 
x: R
x) 
y: R
y :=
  
h: Commute x y
h.
bit0_left: ∀ {R : Type ?u.1523} [inst : Distrib R] {x y : R}, Commute x y → Commute (bit0 x) y
bit0_left.
add_left: ∀ {R : Type ?u.1566} [inst : Distrib R] {a b c : R}, Commute a c → Commute b c → Commute (a + b) c
add_left (
Commute.one_left: ∀ {M : Type ?u.1585} [inst : MulOneClass M] (a : M), Commute 1 a
Commute.one_left 
y: R
y)
#align commute.bit1_left 
Commute.bit1_left: ∀ {R : Type x} [inst : NonAssocSemiring R] {x y : R}, Commute x y → Commute (bit1 x) y
Commute.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.1617
NonUnitalNonAssocRing 
R: Type x
R] {
a: R
a 
b: R
b : 
R: Type x
R} (
h: Commute a b
h : 
Commute: {S : Type ?u.1624} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a 
b: R
b) :
    
a: R
a * 
a: R
a - 
b: R
b * 
b: R
b = (
a: R
a + 
b: R
b) * (
a: R
a - 
b: R
b) := by
Goals accomplished! 🐙
  
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = (a + b) * (a - b)rw [
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * 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 * c
add_mul,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = a * (a - b) + b * (a - b) 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = (a + b) * (a - b)
mul_sub: ∀ {α : Type ?u.2241} [inst : NonUnitalNonAssocRing α] (a b c : α), a * (b - c) = a * b - a * c
mul_sub,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = a * a - a * b + b * (a - b) 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = (a + b) * (a - b)
mul_sub: ∀ {α : Type ?u.2283} [inst : NonUnitalNonAssocRing α] (a b c : α), a * (b - c) = a * b - a * c
mul_sub,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = a * a - a * b + (b * a - b * b) 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = (a + b) * (a - b)
h: Commute a b
h.
eq: ∀ {S : Type ?u.2308} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = a * a - b * a + (b * a - b * b) 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * 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 - c
sub_add_sub_cancel
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * 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.2407
NonUnitalNonAssocRing 
R: Type x
R] {
a: R
a 
b: R
b : 
R: Type x
R} (
h: Commute a b
h : 
Commute: {S : Type ?u.2414} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a 
b: R
b) :
    
a: R
a * 
a: R
a - 
b: R
b * 
b: R
b = (
a: R
a - 
b: R
b) * (
a: R
a + 
b: R
b) := by
Goals accomplished! 🐙
  
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = (a - b) * (a + b)rw [
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * 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 * c
mul_add,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = (a - b) * a + (a - b) * b 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = (a - b) * (a + b)
sub_mul: ∀ {α : Type ?u.3025} [inst : NonUnitalNonAssocRing α] (a b c : α), (a - b) * c = a * c - b * c
sub_mul,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = a * a - b * a + (a - b) * b 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = (a - b) * (a + b)
sub_mul: ∀ {α : Type ?u.3073} [inst : NonUnitalNonAssocRing α] (a b c : α), (a - b) * c = a * c - b * c
sub_mul,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = a * a - b * a + (a * b - b * b) 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = (a - b) * (a + b)
h: Commute a b
h.
eq: ∀ {S : Type ?u.3104} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * a - b * b = a * a - b * a + (b * a - b * b) 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * 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 - c
sub_add_sub_cancel
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonUnitalNonAssocRing R

a, b: R

h: Commute a b

a * 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.3203
NonUnitalNonAssocRing 
R: Type x
R] [
NoZeroDivisors: (M₀ : Type ?u.3206) → [inst : Mul M₀] → [inst : Zero M₀] → Prop
NoZeroDivisors 
R: Type x
R] {
a: R
a 
b: R
b : 
R: Type x
R}
    (
h: Commute a b
h : 
Commute: {S : Type ?u.3388} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a 
b: R
b) : 
a: R
a * 
a: R
a = 
b: R
b * 
b: R
b ↔ 
a: R
a = 
b: R
b ∨ 
a: R
a = -
b: R
b := by
Goals accomplished! 🐙
  
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a * a = b * b ↔ a = b ∨ a = -brw [
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a * a = b * b ↔ a = b ∨ a = -b← 
sub_eq_zero: ∀ {G : Type ?u.3583} [inst : AddGroup G] {a b : G}, a - b = 0 ↔ a = b
sub_eq_zero,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a * a - b * b = 0 ↔ a = b ∨ a = -b 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a * a = b * b ↔ a = b ∨ a = -b
h: Commute a b
h.
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 w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

(a + b) * (a - b) = 0 ↔ a = b ∨ a = -b 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a * a = b * b ↔ a = b ∨ a = -b
mul_eq_zero: ∀ {M₀ : Type ?u.3663} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, a * b = 0 ↔ a = 0 ∨ b = 0
mul_eq_zero,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a * a = b * b ↔ a = b ∨ a = -b
or_comm: ∀ {a b : Prop}, a ∨ b ↔ b ∨ a
or_comm,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a - b = 0 ∨ a + b = 0 ↔ a = b ∨ a = -b 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a * a = b * b ↔ a = b ∨ a = -b
sub_eq_zero: ∀ {G : Type ?u.3747} [inst : AddGroup G] {a b : G}, a - b = 0 ↔ a = b
sub_eq_zero,
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a = b ∨ a + b = 0 ↔ a = b ∨ a = -b
    
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a * a = b * b ↔ a = b ∨ a = -b
add_eq_zero_iff_eq_neg: ∀ {G : Type ?u.3782} [inst : AddGroup G] {a b : G}, a + b = 0 ↔ a = -b
add_eq_zero_iff_eq_neg
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonUnitalNonAssocRing R

inst✝: NoZeroDivisors R

a, b: R

h: Commute a b

a = 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.3879
Mul 
R: Type x
R] [
HasDistribNeg: (α : Type ?u.4253) → [inst : Mul α] → Type ?u.4253
HasDistribNeg 
R: Type x
R] {
a: R
a 
b: R
b : 
R: Type x
R}

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 → Prop
Commute 
a: R
a 
b: R
b → 
Commute: {S : Type ?u.3923} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a (-
b: R
b) :=
  
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 b
neg_right_iff : 
Commute: {S : Type ?u.4270} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a (-
b: R
b) ↔ 
Commute: {S : Type ?u.4544} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a 
b: R
b :=
  
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 y
SemiconjBy.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 b
Commute.neg_right_iff

theorem 
neg_left: ∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute a b → Commute (-a) b
neg_left : 
Commute: {S : Type ?u.4644} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a 
b: R
b → 
Commute: {S : Type ?u.4667} → [inst : Mul S] → S → S → Prop
Commute (-
a: R
a) 
b: R
b :=
  
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 y
SemiconjBy.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) b
Commute.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 b
neg_left_iff : 
Commute: {S : Type ?u.5014} → [inst : Mul S] → S → S → Prop
Commute (-
a: R
a) 
b: R
b ↔ 
Commute: {S : Type ?u.5288} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a 
b: R
b :=
  
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 y
SemiconjBy.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 b
Commute.neg_left_iff

end

section

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

-- 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: R
a : 
R: Type x
R) : 
Commute: {S : Type ?u.5747} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a (-
1: ?m.5762
1) :=
  
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: R
a
#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) a
neg_one_left (
a: R
a : 
R: Type x
R) : 
Commute: {S : Type ?u.6632} → [inst : Mul S] → S → S → Prop
Commute (-
1: ?m.6647
1) 
a: R
a :=
  
SemiconjBy.neg_one_left: ∀ {R : Type ?u.7321} [inst : MulOneClass R] [inst_1 : HasDistribNeg R] (x : R), SemiconjBy (-1) x x
SemiconjBy.neg_one_left 
a: R
a
#align commute.neg_one_left 
Commute.neg_one_left: ∀ {R : Type x} [inst : MulOneClass R] [inst_1 : HasDistribNeg R] (a : R), Commute (-1) a
Commute.neg_one_left

end

section

variable [
NonUnitalNonAssocRing: Type ?u.7360 → Type ?u.7360
NonUnitalNonAssocRing 
R: Type x
R] {
a: R
a 
b: R
b 
c: R
c : 
R: Type x
R}

@[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 → Prop
Commute 
a: R
a 
b: R
b → 
Commute: {S : Type ?u.7401} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a 
c: R
c → 
Commute: {S : Type ?u.7415} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a (
b: R
b - 
c: R
c) :=
  
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) c
sub_left : 
Commute: {S : Type ?u.7655} → [inst : Mul S] → S → S → Prop
Commute 
a: R
a 
c: R
c → 
Commute: {S : Type ?u.7686} → [inst : Mul S] → S → S → Prop
Commute 
b: R
b 
c: R
c → 
Commute: {S : Type ?u.7700} → [inst : Mul S] → S → S → Prop
Commute (
a: R
a - 
b: R
b) 
c: R
c :=
  
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 y
SemiconjBy.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) c
Commute.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.7929
CommRing 
R: Type x
R] (
a: R
a 
b: R
b : 
R: Type x
R) : 
a: R
a * 
a: R
a - 
b: R
b * 
b: R
b = (
a: R
a + 
b: R
b) * (
a: R
a - 
b: R
b) :=
  (
Commute.all: ∀ {S : Type ?u.8262} [inst : CommSemigroup S] (a b : S), Commute a b
Commute.all 
a: R
a 
b: R
b).
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.8325
NonAssocRing 
R: Type x
R] (
a: R
a : 
R: Type x
R) : 
a: R
a * 
a: R
a - 
1: ?m.8338
1 = (
a: R
a + 
1: ?m.8360
1) * (
a: R
a - 
1: ?m.8374
1) := by
Goals accomplished! 🐙
  
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonAssocRing R

a: R

a * a - 1 = (a + 1) * (a - 1)rw [
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonAssocRing R

a: R

a * a - 1 = (a + 1) * (a - 1)← (
Commute.one_right: ∀ {M : Type ?u.8733} [inst : MulOneClass M] (a : M), Commute a 1
Commute.one_right 
a: R
a).
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 w

R: Type x

inst✝: NonAssocRing R

a: R

a * a - 1 = a * a - 1 * 1 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonAssocRing R

a: R

a * a - 1 = (a + 1) * (a - 1)
mul_one: ∀ {M : Type ?u.8821} [inst : MulOneClass M] (a : M), a * 1 = a
mul_one
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝: NonAssocRing R

a: R

a * 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 = -b
mul_self_eq_mul_self_iff [
CommRing: Type ?u.8871 → Type ?u.8871
CommRing 
R: Type x
R] [
NoZeroDivisors: (M₀ : Type ?u.8874) → [inst : Mul M₀] → [inst : Zero M₀] → Prop
NoZeroDivisors 
R: Type x
R] {
a: R
a 
b: R
b : 
R: Type x
R} :
    
a: R
a * 
a: R
a = 
b: R
b * 
b: R
b ↔ 
a: R
a = 
b: R
b ∨ 
a: R
a = -
b: R
b :=
  (
Commute.all: ∀ {S : Type ?u.9079} [inst : CommSemigroup S] (a b : S), Commute a b
Commute.all 
a: R
a 
b: R
b).
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 = -b
mul_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 = -1
mul_self_eq_one_iff [
NonAssocRing: Type ?u.9152 → Type ?u.9152
NonAssocRing 
R: Type x
R] [
NoZeroDivisors: (M₀ : Type ?u.9155) → [inst : Mul M₀] → [inst : Zero M₀] → Prop
NoZeroDivisors 
R: Type x
R] {
a: R
a : 
R: Type x
R} :
    
a: R
a * 
a: R
a = 
1: ?m.9279
1 ↔ 
a: R
a = 
1: ?m.9394
1 ∨ 
a: R
a = -
1: ?m.9413
1 := by
Goals accomplished! 🐙
  
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonAssocRing R

inst✝: NoZeroDivisors R

a: R

a * a = 1 ↔ a = 1 ∨ a = -1rw [
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonAssocRing R

inst✝: NoZeroDivisors R

a: R

a * a = 1 ↔ a = 1 ∨ a = -1← (
Commute.one_right: ∀ {M : Type ?u.9467} [inst : MulOneClass M] (a : M), Commute a 1
Commute.one_right 
a: R
a).
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 w

R: Type x

inst✝¹: NonAssocRing R

inst✝: NoZeroDivisors R

a: R

a * a = 1 ↔ a * a = 1 * 1 
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonAssocRing R

inst✝: NoZeroDivisors R

a: R

a * a = 1 ↔ a = 1 ∨ a = -1
mul_one: ∀ {M : Type ?u.9548} [inst : MulOneClass M] (a : M), a * 1 = a
mul_one
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: NonAssocRing R

inst✝: NoZeroDivisors R

a: R

a * 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 = -1
mul_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
  one's additive inverse. -/
theorem 
inv_eq_self_iff: ∀ {R : Type x} [inst : Ring R] [inst_1 : NoZeroDivisors R] (u : Rˣ), u⁻¹ = u ↔ u = 1 ∨ u = -1
inv_eq_self_iff [
Ring: Type ?u.9607 → Type ?u.9607
Ring 
R: Type x
R] [
NoZeroDivisors: (M₀ : Type ?u.9610) → [inst : Mul M₀] → [inst : Zero M₀] → Prop
NoZeroDivisors 
R: Type x
R] (
u: Rˣ
u : 
R: Type x
Rˣ) : 
u: Rˣ
u⁻¹ = 
u: Rˣ
u ↔ 
u: Rˣ
u = 
1: ?m.9746
1 ∨ 
u: Rˣ
u = -
1: ?m.9931
1 := by
Goals accomplished! 🐙
  
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: Ring R

inst✝: NoZeroDivisors R

u: Rˣ

u⁻¹ = u ↔ u = 1 ∨ u = -1rw [
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: Ring R

inst✝: NoZeroDivisors R

u: Rˣ

u⁻¹ = u ↔ u = 1 ∨ u = -1
inv_eq_iff_mul_eq_one: ∀ {G : Type ?u.9985} [inst : Group G] {a b : G}, a⁻¹ = b ↔ a * b = 1
inv_eq_iff_mul_eq_one
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: Ring R

inst✝: NoZeroDivisors R

u: Rˣ

u * u = 1 ↔ u = 1 ∨ u = -1]
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: Ring R

inst✝: NoZeroDivisors R

u: Rˣ

u * u = 1 ↔ u = 1 ∨ u = -1
  
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: Ring R

inst✝: NoZeroDivisors R

u: Rˣ

u⁻¹ = u ↔ u = 1 ∨ u = -1simp only [
ext_iff: ∀ {α : Type ?u.10038} [inst : Monoid α] {a b : αˣ}, a = b ↔ ↑a = ↑b
ext_iff]
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: Ring R

inst✝: NoZeroDivisors R

u: Rˣ

↑(u * u) = ↑1 ↔ ↑u = ↑1 ∨ ↑u = ↑(-1)
  
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: Ring R

inst✝: NoZeroDivisors R

u: Rˣ

u⁻¹ = u ↔ u = 1 ∨ u = -1push_cast
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: Ring R

inst✝: NoZeroDivisors R

u: Rˣ

↑u * ↑u = 1 ↔ ↑u = 1 ∨ ↑u = -1
  
α: Type u

β: Type v

γ: Type w

R: Type x

inst✝¹: Ring R

inst✝: NoZeroDivisors R

u: Rˣ

u⁻¹ = u ↔ u = 1 ∨ u = -1exact 
mul_self_eq_one_iff: ∀ {R : Type ?u.10374} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] {a : R}, a * a = 1 ↔ a = 1 ∨ a = -1
mul_self_eq_one_iff
Goals accomplished! 🐙
#align units.inv_eq_self_iff 
Units.inv_eq_self_iff: ∀ {R : Type x} [inst : Ring R] [inst_1 : NoZeroDivisors R] (u : Rˣ), u⁻¹ = u ↔ u = 1 ∨ u = -1
Units.inv_eq_self_iff

end Units