# Documentation

Mathlib.Algebra.Opposites

# Multiplicative opposite and algebraic operations on it #

In this file we define MulOpposite α = αᵐᵒᵖ to be the multiplicative opposite of α. It inherits all additive algebraic structures on α (in other files), and reverses the order of multipliers in multiplicative structures, i.e., op (x * y) = op y * op x, where MulOpposite.op is the canonical map from α to αᵐᵒᵖ.

We also define AddOpposite α = αᵃᵒᵖ to be the additive opposite of α. It inherits all multiplicative algebraic structures on α (in other files), and reverses the order of summands in additive structures, i.e. op (x + y) = op y + op x, where AddOpposite.op is the canonical map from α to αᵃᵒᵖ.

## Notation #

• αᵐᵒᵖ = MulOpposite α
• αᵃᵒᵖ = AddOpposite α

## Implementation notes #

In mathlib3 αᵐᵒᵖ was just a type synonym for α, marked irreducible after the API was developed. In mathlib4 we use a structure with one field, because it is not possible to change the reducibility of a declaration after its definition, and because Lean 4 has definitional eta reduction for structures (Lean 3 does not).

## Tags #

structure MulOpposite (α : Type u) :
• op :: (
• The element of α represented by x : αᵐᵒᵖ.

unop : α
• )

Multiplicative opposite of a type. This type inherits all additive structures on α and reverses left and right in multiplication.

Instances For
structure AddOpposite (α : Type u) :
• op :: (
• The element of α represented by x : αᵃᵒᵖ.

unop : α
• )

Additive opposite of a type. This type inherits all multiplicative structures on α and reverses left and right in addition.

Instances For

Multiplicative opposite of a type.

Equations

Equations
theorem AddOpposite.unop_op {α : Type u_1} (x : α) :
{ unop := x }.unop = x
theorem MulOpposite.unop_op {α : Type u_1} (x : α) :
{ unop := x }.unop = x
@[simp]
theorem AddOpposite.op_unop {α : Type u_1} (x : αᵃᵒᵖ) :
{ unop := x.unop } = x
@[simp]
theorem MulOpposite.op_unop {α : Type u_1} (x : αᵐᵒᵖ) :
{ unop := x.unop } = x
@[simp]
theorem AddOpposite.op_comp_unop {α : Type u_1} :
@[simp]
theorem MulOpposite.op_comp_unop {α : Type u_1} :
MulOpposite.op MulOpposite.unop = id
@[simp]
theorem AddOpposite.unop_comp_op {α : Type u_1} :
@[simp]
theorem MulOpposite.unop_comp_op {α : Type u_1} :
MulOpposite.unop MulOpposite.op = id
def AddOpposite.rec' {α : Type u_1} {F : αᵃᵒᵖSort v} (h : (X : α) → F { unop := X }) (X : αᵃᵒᵖ) :
F X

A recursor for AddOpposite. Use as induction x using AddOpposite.rec.

Equations
• = h X.unop
def MulOpposite.rec' {α : Type u_1} {F : αᵐᵒᵖSort v} (h : (X : α) → F { unop := X }) (X : αᵐᵒᵖ) :
F X

A recursor for MulOpposite. Use as induction x using MulOpposite.rec'.

Equations
• = h X.unop
def AddOpposite.opEquiv {α : Type u_1} :

The canonical bijection between α and αᵃᵒᵖ.

Equations
• AddOpposite.opEquiv = { toFun := AddOpposite.op, invFun := AddOpposite.unop, left_inv := (_ : ∀ (x : α), { unop := x }.unop = x), right_inv := (_ : ∀ (x : αᵃᵒᵖ), { unop := x.unop } = x) }
@[simp]
theorem MulOpposite.opEquiv_symm_apply {α : Type u_1} :
↑(Equiv.symm MulOpposite.opEquiv) = MulOpposite.unop
@[simp]
theorem MulOpposite.opEquiv_apply {α : Type u_1} :
MulOpposite.opEquiv = MulOpposite.op
@[simp]
theorem AddOpposite.opEquiv_apply {α : Type u_1} :
@[simp]
theorem AddOpposite.opEquiv_symm_apply {α : Type u_1} :
def MulOpposite.opEquiv {α : Type u_1} :

The canonical bijection between α and αᵐᵒᵖ.

Equations
• MulOpposite.opEquiv = { toFun := MulOpposite.op, invFun := MulOpposite.unop, left_inv := (_ : ∀ (x : α), { unop := x }.unop = x), right_inv := (_ : ∀ (x : αᵐᵒᵖ), { unop := x.unop } = x) }
theorem AddOpposite.op_bijective {α : Type u_1} :
theorem MulOpposite.op_bijective {α : Type u_1} :
Function.Bijective MulOpposite.op
theorem AddOpposite.unop_bijective {α : Type u_1} :
theorem MulOpposite.unop_bijective {α : Type u_1} :
Function.Bijective MulOpposite.unop
theorem AddOpposite.op_injective {α : Type u_1} :
theorem MulOpposite.op_injective {α : Type u_1} :
Function.Injective MulOpposite.op
theorem AddOpposite.unop_injective {α : Type u_1} :
theorem MulOpposite.unop_injective {α : Type u_1} :
Function.Injective MulOpposite.unop
theorem AddOpposite.op_inj {α : Type u_1} {x : α} {y : α} :
{ unop := x } = { unop := y } x = y
theorem MulOpposite.op_inj {α : Type u_1} {x : α} {y : α} :
{ unop := x } = { unop := y } x = y
@[simp]
theorem AddOpposite.unop_inj {α : Type u_1} {x : αᵃᵒᵖ} {y : αᵃᵒᵖ} :
x.unop = y.unop x = y
@[simp]
theorem MulOpposite.unop_inj {α : Type u_1} {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} :
x.unop = y.unop x = y
def AddOpposite.nontrivial.proof_1 (α : Type u_1) [inst : ] :
Equations
• (_ : ) = (_ : )
instance AddOpposite.nontrivial (α : Type u_1) [inst : ] :
Equations
instance MulOpposite.nontrivial (α : Type u_1) [inst : ] :
Equations
instance AddOpposite.inhabited (α : Type u_1) [inst : ] :
Equations
• = { default := { unop := default } }
instance MulOpposite.inhabited (α : Type u_1) [inst : ] :
Equations
• = { default := { unop := default } }
def AddOpposite.subsingleton.proof_1 (α : Type u_1) [inst : ] :
Equations
• (_ : ) = (_ : )
instance AddOpposite.subsingleton (α : Type u_1) [inst : ] :
Equations
instance MulOpposite.subsingleton (α : Type u_1) [inst : ] :
Equations
instance AddOpposite.unique (α : Type u_1) [inst : ] :
Equations
def AddOpposite.unique.proof_1 (α : Type u_1) [inst : ] :
Equations
• (_ : ) = (_ : )
instance MulOpposite.unique (α : Type u_1) [inst : ] :
Equations
def AddOpposite.isEmpty.proof_1 (α : Type u_1) [inst : ] :
Equations
• (_ : ) = (_ : )
instance AddOpposite.isEmpty (α : Type u_1) [inst : ] :
Equations
instance MulOpposite.isEmpty (α : Type u_1) [inst : ] :
Equations
instance MulOpposite.zero (α : Type u_1) [inst : Zero α] :
Equations
• = { zero := { unop := 0 } }
instance AddOpposite.zero (α : Type u_1) [inst : Zero α] :
Equations
• = { zero := { unop := 0 } }
instance MulOpposite.one (α : Type u_1) [inst : One α] :
Equations
• = { one := { unop := 1 } }
Equations
• = { add := fun x y => { unop := x.unop + y.unop } }
instance MulOpposite.sub (α : Type u_1) [inst : Sub α] :
Equations
• = { sub := fun x y => { unop := x.unop - y.unop } }
instance MulOpposite.neg (α : Type u_1) [inst : Neg α] :
Equations
• = { neg := fun x => { unop := -x.unop } }
instance MulOpposite.involutiveNeg (α : Type u_1) [inst : ] :
Equations
Equations
• = { add := fun x y => { unop := y.unop + x.unop } }
instance MulOpposite.mul (α : Type u_1) [inst : Mul α] :
Equations
• = { mul := fun x y => { unop := y.unop * x.unop } }
instance AddOpposite.neg (α : Type u_1) [inst : Neg α] :
Equations
• = { neg := fun x => { unop := -x.unop } }
instance MulOpposite.inv (α : Type u_1) [inst : Inv α] :
Equations
• = { inv := fun x => { unop := x.unop⁻¹ } }
def AddOpposite.involutiveNeg.proof_1 (α : Type u_1) [inst : ] :
∀ (x : αᵃᵒᵖ), - -x = x
Equations
instance AddOpposite.involutiveNeg (α : Type u_1) [inst : ] :
Equations
instance MulOpposite.involutiveInv (α : Type u_1) [inst : ] :
Equations
Equations
• = { vadd := fun c x => { unop := c +ᵥ x.unop } }
instance MulOpposite.smul (α : Type u_1) (R : Type u_2) [inst : SMul R α] :
Equations
• = { smul := fun c x => { unop := c x.unop } }
@[simp]
theorem MulOpposite.op_zero (α : Type u_1) [inst : Zero α] :
{ unop := 0 } = 0
@[simp]
theorem MulOpposite.unop_zero (α : Type u_1) [inst : Zero α] :
0.unop = 0
@[simp]
theorem AddOpposite.op_zero (α : Type u_1) [inst : Zero α] :
{ unop := 0 } = 0
@[simp]
theorem MulOpposite.op_one (α : Type u_1) [inst : One α] :
{ unop := 1 } = 1
@[simp]
theorem AddOpposite.unop_zero (α : Type u_1) [inst : Zero α] :
0.unop = 0
@[simp]
theorem MulOpposite.unop_one (α : Type u_1) [inst : One α] :
1.unop = 1
@[simp]
theorem MulOpposite.op_add {α : Type u_1} [inst : Add α] (x : α) (y : α) :
{ unop := x + y } = { unop := x } + { unop := y }
@[simp]
theorem MulOpposite.unop_add {α : Type u_1} [inst : Add α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) :
(x + y).unop = x.unop + y.unop
@[simp]
theorem MulOpposite.op_neg {α : Type u_1} [inst : Neg α] (x : α) :
{ unop := -x } = -{ unop := x }
@[simp]
theorem MulOpposite.unop_neg {α : Type u_1} [inst : Neg α] (x : αᵐᵒᵖ) :
(-x).unop = -x.unop
@[simp]
theorem AddOpposite.op_add {α : Type u_1} [inst : Add α] (x : α) (y : α) :
{ unop := x + y } = { unop := y } + { unop := x }
@[simp]
theorem MulOpposite.op_mul {α : Type u_1} [inst : Mul α] (x : α) (y : α) :
{ unop := x * y } = { unop := y } * { unop := x }
@[simp]
theorem AddOpposite.unop_add {α : Type u_1} [inst : Add α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) :
(x + y).unop = y.unop + x.unop
@[simp]
theorem MulOpposite.unop_mul {α : Type u_1} [inst : Mul α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) :
(x * y).unop = y.unop * x.unop
@[simp]
theorem AddOpposite.op_neg {α : Type u_1} [inst : Neg α] (x : α) :
{ unop := -x } = -{ unop := x }
@[simp]
theorem MulOpposite.op_inv {α : Type u_1} [inst : Inv α] (x : α) :
{ unop := x⁻¹ } = { unop := x }⁻¹
@[simp]
theorem AddOpposite.unop_neg {α : Type u_1} [inst : Neg α] (x : αᵃᵒᵖ) :
(-x).unop = -x.unop
@[simp]
theorem MulOpposite.unop_inv {α : Type u_1} [inst : Inv α] (x : αᵐᵒᵖ) :
x⁻¹.unop = x.unop⁻¹
@[simp]
theorem MulOpposite.op_sub {α : Type u_1} [inst : Sub α] (x : α) (y : α) :
{ unop := x - y } = { unop := x } - { unop := y }
@[simp]
theorem MulOpposite.unop_sub {α : Type u_1} [inst : Sub α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) :
(x - y).unop = x.unop - y.unop
@[simp]
theorem AddOpposite.op_vadd {α : Type u_2} {R : Type u_1} [inst : VAdd R α] (c : R) (a : α) :
{ unop := c +ᵥ a } = c +ᵥ { unop := a }
@[simp]
theorem MulOpposite.op_smul {α : Type u_2} {R : Type u_1} [inst : SMul R α] (c : R) (a : α) :
{ unop := c a } = c { unop := a }
@[simp]
theorem AddOpposite.unop_vadd {α : Type u_2} {R : Type u_1} [inst : VAdd R α] (c : R) (a : αᵃᵒᵖ) :
(c +ᵥ a).unop = c +ᵥ a.unop
@[simp]
theorem MulOpposite.unop_smul {α : Type u_2} {R : Type u_1} [inst : SMul R α] (c : R) (a : αᵐᵒᵖ) :
(c a).unop = c a.unop
@[simp]
theorem MulOpposite.unop_eq_zero_iff {α : Type u_1} [inst : Zero α] (a : αᵐᵒᵖ) :
a.unop = 0 a = 0
@[simp]
theorem MulOpposite.op_eq_zero_iff {α : Type u_1} [inst : Zero α] (a : α) :
{ unop := a } = 0 a = 0
theorem MulOpposite.unop_ne_zero_iff {α : Type u_1} [inst : Zero α] (a : αᵐᵒᵖ) :
a.unop 0 a 0
theorem MulOpposite.op_ne_zero_iff {α : Type u_1} [inst : Zero α] (a : α) :
{ unop := a } 0 a 0
@[simp]
theorem AddOpposite.unop_eq_zero_iff {α : Type u_1} [inst : Zero α] (a : αᵃᵒᵖ) :
a.unop = 0 a = 0
@[simp]
theorem MulOpposite.unop_eq_one_iff {α : Type u_1} [inst : One α] (a : αᵐᵒᵖ) :
a.unop = 1 a = 1
@[simp]
theorem AddOpposite.op_eq_zero_iff {α : Type u_1} [inst : Zero α] (a : α) :
{ unop := a } = 0 a = 0
@[simp]
theorem MulOpposite.op_eq_one_iff {α : Type u_1} [inst : One α] (a : α) :
{ unop := a } = 1 a = 1
instance AddOpposite.one {α : Type u_1} [inst : One α] :
Equations
• AddOpposite.one = { one := { unop := 1 } }
@[simp]
theorem AddOpposite.op_one {α : Type u_1} [inst : One α] :
{ unop := 1 } = 1
@[simp]
theorem AddOpposite.unop_one {α : Type u_1} [inst : One α] :
1.unop = 1
@[simp]
theorem AddOpposite.op_eq_one_iff {α : Type u_1} [inst : One α] {a : α} :
{ unop := a } = 1 a = 1
@[simp]
theorem AddOpposite.unop_eq_one_iff {α : Type u_1} [inst : One α] {a : αᵃᵒᵖ} :
a.unop = 1 a = 1
instance AddOpposite.mul {α : Type u_1} [inst : Mul α] :
Equations
• AddOpposite.mul = { mul := fun a b => { unop := a.unop * b.unop } }
@[simp]
theorem AddOpposite.op_mul {α : Type u_1} [inst : Mul α] (a : α) (b : α) :
{ unop := a * b } = { unop := a } * { unop := b }
@[simp]
theorem AddOpposite.unop_mul {α : Type u_1} [inst : Mul α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
(a * b).unop = a.unop * b.unop
instance AddOpposite.inv {α : Type u_1} [inst : Inv α] :
Equations
• AddOpposite.inv = { inv := fun a => { unop := a.unop⁻¹ } }
instance AddOpposite.involutiveInv {α : Type u_1} [inst : ] :
Equations
@[simp]
theorem AddOpposite.op_inv {α : Type u_1} [inst : Inv α] (a : α) :
{ unop := a⁻¹ } = { unop := a }⁻¹
@[simp]
theorem AddOpposite.unop_inv {α : Type u_1} [inst : Inv α] (a : αᵃᵒᵖ) :
a⁻¹.unop = a.unop⁻¹
instance AddOpposite.div {α : Type u_1} [inst : Div α] :
Equations
• AddOpposite.div = { div := fun a b => { unop := a.unop / b.unop } }
@[simp]
theorem AddOpposite.op_div {α : Type u_1} [inst : Div α] (a : α) (b : α) :
{ unop := a / b } = { unop := a } / { unop := b }
@[simp]
theorem AddOpposite.unop_div {α : Type u_1} [inst : Div α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
(a / b).unop = a.unop / b.unop