# 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 PreOpposite (α : Type u_3) :
Type u_3

Auxiliary type to implement MulOpposite and AddOpposite.

It turns out to be convenient to have MulOpposite α = AddOpposite α true by definition, in the same way that it is convenient to have Additive α = α; this means that we also get the defeq AddOpposite (Additive α) = MulOpposite α, which is convenient when working with quotients.

This is a compromise between making MulOpposite α = AddOpposite α = α (what we had in Lean 3) and having no defeqs within those three types (which we had as of mathlib4#1036).

• op' :: (
• unop' : α

The element of α represented by x : PreOpposite α.

• )
Instances For
def AddOpposite (α : Type u_3) :
Type u_3

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

Equations
Instances For
def MulOpposite (α : Type u_3) :
Type u_3

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

Equations
Instances For

Multiplicative opposite of a type.

Equations
Instances For

Equations
Instances For
def AddOpposite.op {α : Type u_1} :
ααᵃᵒᵖ

The element of αᵃᵒᵖ that represents x : α.

Equations
Instances For
def MulOpposite.op {α : Type u_1} :
ααᵐᵒᵖ

The element of MulOpposite α that represents x : α.

Equations
• MulOpposite.op = PreOpposite.op'
Instances For
def AddOpposite.unop {α : Type u_1} :
αᵃᵒᵖα

The element of α represented by x : αᵃᵒᵖ.

Equations
Instances For
def MulOpposite.unop {α : Type u_1} :
αᵐᵒᵖα

The element of α represented by x : αᵐᵒᵖ.

Equations
• MulOpposite.unop = PreOpposite.unop'
Instances For
@[simp]
theorem AddOpposite.unop_op {α : Type u_1} (x : α) :
@[simp]
theorem MulOpposite.unop_op {α : Type u_1} (x : α) :
@[simp]
theorem AddOpposite.op_unop {α : Type u_1} (x : αᵃᵒᵖ) :
@[simp]
theorem MulOpposite.op_unop {α : Type u_1} (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 u_3} (h : (X : α) → F ()) (X : αᵃᵒᵖ) :
F X

A recursor for AddOpposite. Use as induction x.

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

A recursor for MulOpposite. Use as induction x.

Equations
• = h ()
Instances For
def AddOpposite.opEquiv {α : Type u_1} :

The canonical bijection between α and αᵃᵒᵖ.

Equations
Instances For
@[simp]
theorem AddOpposite.opEquiv_apply {α : Type u_1} :
@[simp]
theorem AddOpposite.opEquiv_symm_apply {α : Type u_1} :
@[simp]
theorem MulOpposite.opEquiv_apply {α : Type u_1} :
MulOpposite.opEquiv = MulOpposite.op
@[simp]
theorem MulOpposite.opEquiv_symm_apply {α : Type u_1} :
MulOpposite.opEquiv.symm = MulOpposite.unop
def MulOpposite.opEquiv {α : Type u_1} :

The canonical bijection between α and αᵐᵒᵖ.

Equations
• MulOpposite.opEquiv = { toFun := MulOpposite.op, invFun := MulOpposite.unop, left_inv := , right_inv := }
Instances For
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.op_surjective {α : Type u_1} :
theorem MulOpposite.op_surjective {α : Type u_1} :
Function.Surjective MulOpposite.op
theorem AddOpposite.unop_injective {α : Type u_1} :
theorem MulOpposite.unop_injective {α : Type u_1} :
Function.Injective MulOpposite.unop
theorem AddOpposite.unop_surjective {α : Type u_1} :
theorem MulOpposite.unop_surjective {α : Type u_1} :
Function.Surjective MulOpposite.unop
@[simp]
theorem AddOpposite.op_inj {α : Type u_1} {x : α} {y : α} :
x = y
@[simp]
theorem MulOpposite.op_inj {α : Type u_1} {x : α} {y : α} :
x = y
@[simp]
theorem AddOpposite.unop_inj {α : Type u_1} {x : αᵃᵒᵖ} {y : αᵃᵒᵖ} :
x = y
@[simp]
theorem MulOpposite.unop_inj {α : Type u_1} {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} :
x = y
instance AddOpposite.instNontrivial {α : Type u_1} [] :
Equations
• =
instance MulOpposite.instNontrivial {α : Type u_1} [] :
Equations
• =
instance AddOpposite.instInhabited {α : Type u_1} [] :
Equations
instance MulOpposite.instInhabited {α : Type u_1} [] :
Equations
instance AddOpposite.instSubsingleton {α : Type u_1} [] :
Equations
• =
instance MulOpposite.instSubsingleton {α : Type u_1} [] :
Equations
• =
instance AddOpposite.instUnique {α : Type u_1} [] :
Equations
instance MulOpposite.instUnique {α : Type u_1} [] :
Equations
• MulOpposite.instUnique =
instance AddOpposite.instIsEmpty {α : Type u_1} [] :
Equations
• =
instance MulOpposite.instIsEmpty {α : Type u_1} [] :
Equations
• =
instance AddOpposite.instDecidableEq {α : Type u_1} [] :
Equations
instance MulOpposite.instDecidableEq {α : Type u_1} [] :
Equations
• MulOpposite.instDecidableEq = .decidableEq
instance MulOpposite.instZero {α : Type u_1} [Zero α] :
Equations
• MulOpposite.instZero = { zero := }
instance AddOpposite.instZero {α : Type u_1} [Zero α] :
Equations
• AddOpposite.instZero = { zero := }
instance MulOpposite.instOne {α : Type u_1} [One α] :
Equations
• MulOpposite.instOne = { one := }
Equations
• MulOpposite.instAdd = { add := fun (x y : αᵐᵒᵖ) => }
instance MulOpposite.instSub {α : Type u_1} [Sub α] :
Equations
• MulOpposite.instSub = { sub := fun (x y : αᵐᵒᵖ) => }
instance MulOpposite.instNeg {α : Type u_1} [Neg α] :
Equations
• MulOpposite.instNeg = { neg := fun (x : αᵐᵒᵖ) => }
instance MulOpposite.instInvolutiveNeg {α : Type u_1} [] :
Equations
• MulOpposite.instInvolutiveNeg =
Equations
instance MulOpposite.instMul {α : Type u_1} [Mul α] :
Equations
• MulOpposite.instMul = { mul := fun (x y : αᵐᵒᵖ) => }
instance AddOpposite.instNeg {α : Type u_1} [Neg α] :
Equations
• AddOpposite.instNeg = { neg := fun (x : αᵃᵒᵖ) => }
instance MulOpposite.instInv {α : Type u_1} [Inv α] :
Equations
• MulOpposite.instInv = { inv := fun (x : αᵐᵒᵖ) => }
instance AddOpposite.instInvolutiveNeg {α : Type u_1} [] :
Equations
theorem AddOpposite.instInvolutiveNeg.proof_1 {α : Type u_1} [] :
∀ (x : αᵃᵒᵖ), - -x = x
instance MulOpposite.instInvolutiveInv {α : Type u_1} [] :
Equations
• MulOpposite.instInvolutiveInv =
Equations
instance MulOpposite.instSMul {α : Type u_1} {β : Type u_2} [SMul α β] :
Equations
• MulOpposite.instSMul = { smul := fun (c : α) (x : βᵐᵒᵖ) => }
@[simp]
theorem MulOpposite.op_zero {α : Type u_1} [Zero α] :
@[simp]
theorem MulOpposite.unop_zero {α : Type u_1} [Zero α] :
@[simp]
theorem AddOpposite.op_zero {α : Type u_1} [Zero α] :
@[simp]
theorem MulOpposite.op_one {α : Type u_1} [One α] :
@[simp]
theorem AddOpposite.unop_zero {α : Type u_1} [Zero α] :
@[simp]
theorem MulOpposite.unop_one {α : Type u_1} [One α] :
@[simp]
theorem MulOpposite.op_add {α : Type u_1} [Add α] (x : α) (y : α) :
@[simp]
theorem MulOpposite.unop_add {α : Type u_1} [Add α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) :
@[simp]
theorem MulOpposite.op_neg {α : Type u_1} [Neg α] (x : α) :
@[simp]
theorem MulOpposite.unop_neg {α : Type u_1} [Neg α] (x : αᵐᵒᵖ) :
@[simp]
@[simp]
theorem MulOpposite.op_mul {α : Type u_1} [Mul α] (x : α) (y : α) :
@[simp]
@[simp]
theorem MulOpposite.unop_mul {α : Type u_1} [Mul α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) :
@[simp]
theorem AddOpposite.op_neg {α : Type u_1} [Neg α] (x : α) :
@[simp]
theorem MulOpposite.op_inv {α : Type u_1} [Inv α] (x : α) :
@[simp]
theorem AddOpposite.unop_neg {α : Type u_1} [Neg α] (x : αᵃᵒᵖ) :
@[simp]
theorem MulOpposite.unop_inv {α : Type u_1} [Inv α] (x : αᵐᵒᵖ) :
@[simp]
theorem MulOpposite.op_sub {α : Type u_1} [Sub α] (x : α) (y : α) :
@[simp]
theorem MulOpposite.unop_sub {α : Type u_1} [Sub α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) :
@[simp]
theorem AddOpposite.op_vadd {α : Type u_1} {β : Type u_2} [VAdd α β] (a : α) (b : β) :
@[simp]
theorem MulOpposite.op_smul {α : Type u_1} {β : Type u_2} [SMul α β] (a : α) (b : β) :
@[simp]
theorem AddOpposite.unop_vadd {α : Type u_1} {β : Type u_2} [VAdd α β] (a : α) (b : βᵃᵒᵖ) :
@[simp]
theorem MulOpposite.unop_smul {α : Type u_1} {β : Type u_2} [SMul α β] (a : α) (b : βᵐᵒᵖ) :
@[simp]
theorem MulOpposite.unop_eq_zero_iff {α : Type u_1} [Zero α] (a : αᵐᵒᵖ) :
a = 0
@[simp]
theorem MulOpposite.op_eq_zero_iff {α : Type u_1} [Zero α] (a : α) :
a = 0
theorem MulOpposite.unop_ne_zero_iff {α : Type u_1} [Zero α] (a : αᵐᵒᵖ) :
a 0
theorem MulOpposite.op_ne_zero_iff {α : Type u_1} [Zero α] (a : α) :
a 0
@[simp]
theorem AddOpposite.unop_eq_zero_iff {α : Type u_1} [Zero α] (a : αᵃᵒᵖ) :
a = 0
@[simp]
theorem MulOpposite.unop_eq_one_iff {α : Type u_1} [One α] (a : αᵐᵒᵖ) :
a = 1
@[simp]
theorem AddOpposite.op_eq_zero_iff {α : Type u_1} [Zero α] (a : α) :
a = 0
@[simp]
theorem MulOpposite.op_eq_one_iff {α : Type u_1} [One α] (a : α) :
a = 1
instance AddOpposite.instOne {α : Type u_1} [One α] :
Equations
• AddOpposite.instOne = { one := }
@[simp]
theorem AddOpposite.op_one {α : Type u_1} [One α] :
@[simp]
theorem AddOpposite.unop_one {α : Type u_1} [One α] :
@[simp]
theorem AddOpposite.op_eq_one_iff {α : Type u_1} [One α] {a : α} :
a = 1
@[simp]
theorem AddOpposite.unop_eq_one_iff {α : Type u_1} [One α] {a : αᵃᵒᵖ} :
a = 1
instance AddOpposite.instMul {α : Type u_1} [Mul α] :
Equations
• AddOpposite.instMul = { mul := fun (a b : αᵃᵒᵖ) => }
@[simp]
theorem AddOpposite.op_mul {α : Type u_1} [Mul α] (a : α) (b : α) :
@[simp]
theorem AddOpposite.unop_mul {α : Type u_1} [Mul α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
instance AddOpposite.instInv {α : Type u_1} [Inv α] :
Equations
• AddOpposite.instInv = { inv := fun (a : αᵃᵒᵖ) => }
instance AddOpposite.instInvolutiveInv {α : Type u_1} [] :
Equations