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

multiplicative opposite, additive opposite

structure PreOpposite (α : Type u) : Type u

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 α.

• )

def AddOpposite (α : Type u) : Type u

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

Equations

• αᵃᵒᵖ = PreOpposite α

def MulOpposite (α : Type u) : Type u

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

Equations

• αᵐᵒᵖ = PreOpposite α

def «term_ᵐᵒᵖ» : Lean.TrailingParserDescr

Multiplicative opposite of a type.

Equations

• «term_ᵐᵒᵖ» = Lean.ParserDescr.trailingNode `term_ᵐᵒᵖ 1024 1024 (Lean.ParserDescr.symbol "ᵐᵒᵖ")

def «term_ᵃᵒᵖ» : Lean.TrailingParserDescr

Additive opposite of a type.

Equations

• «term_ᵃᵒᵖ» = Lean.ParserDescr.trailingNode `term_ᵃᵒᵖ 1024 1024 (Lean.ParserDescr.symbol "ᵃᵒᵖ")

def AddOpposite.op {α : Type u_1} : α → αᵃᵒᵖ

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

Equations

• AddOpposite.op = PreOpposite.op'

def MulOpposite.op {α : Type u_1} : α → αᵐᵒᵖ

The element of MulOpposite α that represents x : α.

Equations

• MulOpposite.op = PreOpposite.op'

def AddOpposite.unop {α : Type u_1} : αᵃᵒᵖ → α

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

Equations

• AddOpposite.unop = PreOpposite.unop'

def MulOpposite.unop {α : Type u_1} : αᵐᵒᵖ → α

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

Equations

• MulOpposite.unop = PreOpposite.unop'

@[simp]

theorem AddOpposite.unop_op {α : Type u_1} (x : α) : AddOpposite.unop (AddOpposite.op x) = x

@[simp]

theorem MulOpposite.unop_op {α : Type u_1} (x : α) : MulOpposite.unop (MulOpposite.op x) = x

@[simp]

theorem AddOpposite.op_unop {α : Type u_1} (x : αᵃᵒᵖ) : AddOpposite.op (AddOpposite.unop x) = x

@[simp]

theorem MulOpposite.op_unop {α : Type u_1} (x : αᵐᵒᵖ) : MulOpposite.op (MulOpposite.unop x) = x

@[simp]

theorem AddOpposite.op_comp_unop {α : Type u_1} : AddOpposite.op ∘ AddOpposite.unop = id

@[simp]

theorem MulOpposite.op_comp_unop {α : Type u_1} : MulOpposite.op ∘ MulOpposite.unop = id

@[simp]

theorem AddOpposite.unop_comp_op {α : Type u_1} : AddOpposite.unop ∘ AddOpposite.op = id

@[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 (AddOpposite.op X)) (X : αᵃᵒᵖ) : F X

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

Equations

• AddOpposite.rec' h X = h (AddOpposite.unop X)

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

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

Equations

• MulOpposite.rec' h X = h (MulOpposite.unop X)

def AddOpposite.opEquiv {α : Type u_1} : α ≃ αᵃᵒᵖ

The canonical bijection between α and αᵃᵒᵖ.

Equations

• One or more equations did not get rendered due to their size.

@[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

@[simp]

theorem AddOpposite.opEquiv_apply {α : Type u_1} : ⇑AddOpposite.opEquiv = AddOpposite.op

@[simp]

theorem AddOpposite.opEquiv_symm_apply {α : Type u_1} : ⇑AddOpposite.opEquiv.symm = AddOpposite.unop

def MulOpposite.opEquiv {α : Type u_1} : α ≃ αᵐᵒᵖ

The canonical bijection between α and αᵐᵒᵖ.

Equations

• One or more equations did not get rendered due to their size.

theorem AddOpposite.op_bijective {α : Type u_1} : Function.Bijective AddOpposite.op

theorem MulOpposite.op_bijective {α : Type u_1} : Function.Bijective MulOpposite.op

theorem AddOpposite.unop_bijective {α : Type u_1} : Function.Bijective AddOpposite.unop

theorem MulOpposite.unop_bijective {α : Type u_1} : Function.Bijective MulOpposite.unop

theorem AddOpposite.op_injective {α : Type u_1} : Function.Injective AddOpposite.op

theorem MulOpposite.op_injective {α : Type u_1} : Function.Injective MulOpposite.op

theorem AddOpposite.op_surjective {α : Type u_1} : Function.Surjective AddOpposite.op

theorem MulOpposite.op_surjective {α : Type u_1} : Function.Surjective MulOpposite.op

theorem AddOpposite.unop_injective {α : Type u_1} : Function.Injective AddOpposite.unop

theorem MulOpposite.unop_injective {α : Type u_1} : Function.Injective MulOpposite.unop

theorem AddOpposite.unop_surjective {α : Type u_1} : Function.Surjective AddOpposite.unop

theorem MulOpposite.unop_surjective {α : Type u_1} : Function.Surjective MulOpposite.unop

@[simp]

theorem AddOpposite.op_inj {α : Type u_1} {x : α} {y : α} : AddOpposite.op x = AddOpposite.op y ↔ x = y

@[simp]

theorem MulOpposite.op_inj {α : Type u_1} {x : α} {y : α} : MulOpposite.op x = MulOpposite.op y ↔ x = y

@[simp]

theorem AddOpposite.unop_inj {α : Type u_1} {x : αᵃᵒᵖ} {y : αᵃᵒᵖ} : AddOpposite.unop x = AddOpposite.unop y ↔ x = y

@[simp]

theorem MulOpposite.unop_inj {α : Type u_1} {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} : MulOpposite.unop x = MulOpposite.unop y ↔ x = y

instance AddOpposite.nontrivial (α : Type u_1) [Nontrivial α] : Nontrivial αᵃᵒᵖ

Equations

• (_ : Nontrivial αᵃᵒᵖ) = (_ : Nontrivial αᵃᵒᵖ)

instance MulOpposite.nontrivial (α : Type u_1) [Nontrivial α] : Nontrivial αᵐᵒᵖ

Equations

• (_ : Nontrivial αᵐᵒᵖ) = (_ : Nontrivial αᵐᵒᵖ)

instance AddOpposite.inhabited (α : Type u_1) [Inhabited α] : Inhabited αᵃᵒᵖ

Equations

• AddOpposite.inhabited α = { default := AddOpposite.op default }

instance MulOpposite.inhabited (α : Type u_1) [Inhabited α] : Inhabited αᵐᵒᵖ

Equations

• MulOpposite.inhabited α = { default := MulOpposite.op default }

instance AddOpposite.subsingleton (α : Type u_1) [Subsingleton α] : Subsingleton αᵃᵒᵖ

Equations

• (_ : Subsingleton αᵃᵒᵖ) = (_ : Subsingleton αᵃᵒᵖ)

instance MulOpposite.subsingleton (α : Type u_1) [Subsingleton α] : Subsingleton αᵐᵒᵖ

Equations

• (_ : Subsingleton αᵐᵒᵖ) = (_ : Subsingleton αᵐᵒᵖ)

instance AddOpposite.unique (α : Type u_1) [Unique α] : Unique αᵃᵒᵖ

Equations

• AddOpposite.unique α = Unique.mk' αᵃᵒᵖ

theorem AddOpposite.unique.proof_1 (α : Type u_1) [Unique α] : Subsingleton αᵃᵒᵖ

instance MulOpposite.unique (α : Type u_1) [Unique α] : Unique αᵐᵒᵖ

Equations

• MulOpposite.unique α = Unique.mk' αᵐᵒᵖ

instance AddOpposite.isEmpty (α : Type u_1) [IsEmpty α] : IsEmpty αᵃᵒᵖ

Equations

• (_ : IsEmpty αᵃᵒᵖ) = (_ : IsEmpty αᵃᵒᵖ)

instance MulOpposite.isEmpty (α : Type u_1) [IsEmpty α] : IsEmpty αᵐᵒᵖ

Equations

• (_ : IsEmpty αᵐᵒᵖ) = (_ : IsEmpty αᵐᵒᵖ)

instance AddOpposite.instDecidableEq (α : Type u_1) [DecidableEq α] : DecidableEq αᵃᵒᵖ

Equations

• AddOpposite.instDecidableEq α = Function.Injective.decidableEq (_ : Function.Injective AddOpposite.unop)

instance MulOpposite.instDecidableEq (α : Type u_1) [DecidableEq α] : DecidableEq αᵐᵒᵖ

Equations

• MulOpposite.instDecidableEq α = Function.Injective.decidableEq (_ : Function.Injective MulOpposite.unop)

instance MulOpposite.zero (α : Type u_1) [Zero α] : Zero αᵐᵒᵖ

Equations

• MulOpposite.zero α = { zero := MulOpposite.op 0 }

instance AddOpposite.zero (α : Type u_1) [Zero α] : Zero αᵃᵒᵖ

Equations

• AddOpposite.zero α = { zero := AddOpposite.op 0 }

instance MulOpposite.one (α : Type u_1) [One α] : One αᵐᵒᵖ

Equations

• MulOpposite.one α = { one := MulOpposite.op 1 }

instance MulOpposite.add (α : Type u_1) [Add α] : Add αᵐᵒᵖ

Equations

• MulOpposite.add α = { add := fun (x y : αᵐᵒᵖ) => MulOpposite.op (MulOpposite.unop x + MulOpposite.unop y) }

instance MulOpposite.sub (α : Type u_1) [Sub α] : Sub αᵐᵒᵖ

Equations

• MulOpposite.sub α = { sub := fun (x y : αᵐᵒᵖ) => MulOpposite.op (MulOpposite.unop x - MulOpposite.unop y) }

instance MulOpposite.neg (α : Type u_1) [Neg α] : Neg αᵐᵒᵖ

Equations

• MulOpposite.neg α = { neg := fun (x : αᵐᵒᵖ) => MulOpposite.op (-MulOpposite.unop x) }

instance MulOpposite.involutiveNeg (α : Type u_1) [InvolutiveNeg α] : InvolutiveNeg αᵐᵒᵖ

Equations

• MulOpposite.involutiveNeg α = let src := MulOpposite.neg α; InvolutiveNeg.mk (_ : ∀ (x : αᵐᵒᵖ), - -x = x)

instance AddOpposite.add (α : Type u_1) [Add α] : Add αᵃᵒᵖ

Equations

• AddOpposite.add α = { add := fun (x y : αᵃᵒᵖ) => AddOpposite.op (AddOpposite.unop y + AddOpposite.unop x) }

instance MulOpposite.mul (α : Type u_1) [Mul α] : Mul αᵐᵒᵖ

Equations

• MulOpposite.mul α = { mul := fun (x y : αᵐᵒᵖ) => MulOpposite.op (MulOpposite.unop y * MulOpposite.unop x) }

instance AddOpposite.neg (α : Type u_1) [Neg α] : Neg αᵃᵒᵖ

Equations

• AddOpposite.neg α = { neg := fun (x : αᵃᵒᵖ) => AddOpposite.op (-AddOpposite.unop x) }

instance MulOpposite.inv (α : Type u_1) [Inv α] : Inv αᵐᵒᵖ

Equations

• MulOpposite.inv α = { inv := fun (x : αᵐᵒᵖ) => MulOpposite.op (MulOpposite.unop x)⁻¹ }

instance AddOpposite.involutiveNeg (α : Type u_1) [InvolutiveNeg α] : InvolutiveNeg αᵃᵒᵖ

Equations

• AddOpposite.involutiveNeg α = let src := AddOpposite.neg α; InvolutiveNeg.mk (_ : ∀ (x : αᵃᵒᵖ), - -x = x)

theorem AddOpposite.involutiveNeg.proof_1 (α : Type u_1) [InvolutiveNeg α] : ∀ (x : αᵃᵒᵖ), - -x = x

instance MulOpposite.involutiveInv (α : Type u_1) [InvolutiveInv α] : InvolutiveInv αᵐᵒᵖ

Equations

• MulOpposite.involutiveInv α = let src := MulOpposite.inv α; InvolutiveInv.mk (_ : ∀ (x : αᵐᵒᵖ), x⁻¹⁻¹ = x)

instance AddOpposite.vadd (α : Type u_1) (R : Type u_2) [VAdd R α] : VAdd R αᵃᵒᵖ

Equations

• AddOpposite.vadd α R = { vadd := fun (c : R) (x : αᵃᵒᵖ) => AddOpposite.op (c +ᵥ AddOpposite.unop x) }

instance MulOpposite.smul (α : Type u_1) (R : Type u_2) [SMul R α] : SMul R αᵐᵒᵖ

Equations

• MulOpposite.smul α R = { smul := fun (c : R) (x : αᵐᵒᵖ) => MulOpposite.op (c • MulOpposite.unop x) }

@[simp]

theorem MulOpposite.op_zero (α : Type u_1) [Zero α] : MulOpposite.op 0 = 0

@[simp]

theorem MulOpposite.unop_zero (α : Type u_1) [Zero α] : MulOpposite.unop 0 = 0

@[simp]

theorem AddOpposite.op_zero (α : Type u_1) [Zero α] : AddOpposite.op 0 = 0

@[simp]

theorem MulOpposite.op_one (α : Type u_1) [One α] : MulOpposite.op 1 = 1

@[simp]

theorem AddOpposite.unop_zero (α : Type u_1) [Zero α] : AddOpposite.unop 0 = 0

@[simp]

theorem MulOpposite.unop_one (α : Type u_1) [One α] : MulOpposite.unop 1 = 1

@[simp]

theorem MulOpposite.op_add {α : Type u_1} [Add α] (x : α) (y : α) : MulOpposite.op (x + y) = MulOpposite.op x + MulOpposite.op y

@[simp]

theorem MulOpposite.unop_add {α : Type u_1} [Add α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) : MulOpposite.unop (x + y) = MulOpposite.unop x + MulOpposite.unop y

@[simp]

theorem MulOpposite.op_neg {α : Type u_1} [Neg α] (x : α) : MulOpposite.op (-x) = -MulOpposite.op x

@[simp]

theorem MulOpposite.unop_neg {α : Type u_1} [Neg α] (x : αᵐᵒᵖ) : MulOpposite.unop (-x) = -MulOpposite.unop x

@[simp]

theorem AddOpposite.op_add {α : Type u_1} [Add α] (x : α) (y : α) : AddOpposite.op (x + y) = AddOpposite.op y + AddOpposite.op x

@[simp]

theorem MulOpposite.op_mul {α : Type u_1} [Mul α] (x : α) (y : α) : MulOpposite.op (x * y) = MulOpposite.op y * MulOpposite.op x

@[simp]

theorem AddOpposite.unop_add {α : Type u_1} [Add α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) : AddOpposite.unop (x + y) = AddOpposite.unop y + AddOpposite.unop x

@[simp]

theorem MulOpposite.unop_mul {α : Type u_1} [Mul α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) : MulOpposite.unop (x * y) = MulOpposite.unop y * MulOpposite.unop x

@[simp]

theorem AddOpposite.op_neg {α : Type u_1} [Neg α] (x : α) : AddOpposite.op (-x) = -AddOpposite.op x

@[simp]

theorem MulOpposite.op_inv {α : Type u_1} [Inv α] (x : α) : MulOpposite.op x⁻¹ = (MulOpposite.op x)⁻¹

@[simp]

theorem AddOpposite.unop_neg {α : Type u_1} [Neg α] (x : αᵃᵒᵖ) : AddOpposite.unop (-x) = -AddOpposite.unop x

@[simp]

theorem MulOpposite.unop_inv {α : Type u_1} [Inv α] (x : αᵐᵒᵖ) : MulOpposite.unop x⁻¹ = (MulOpposite.unop x)⁻¹

@[simp]

theorem MulOpposite.op_sub {α : Type u_1} [Sub α] (x : α) (y : α) : MulOpposite.op (x - y) = MulOpposite.op x - MulOpposite.op y

@[simp]

theorem MulOpposite.unop_sub {α : Type u_1} [Sub α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) : MulOpposite.unop (x - y) = MulOpposite.unop x - MulOpposite.unop y

@[simp]

theorem AddOpposite.op_vadd {α : Type u_1} {R : Type u_2} [VAdd R α] (c : R) (a : α) : AddOpposite.op (c +ᵥ a) = c +ᵥ AddOpposite.op a

@[simp]

theorem MulOpposite.op_smul {α : Type u_1} {R : Type u_2} [SMul R α] (c : R) (a : α) : MulOpposite.op (c • a) = c • MulOpposite.op a

@[simp]

theorem AddOpposite.unop_vadd {α : Type u_1} {R : Type u_2} [VAdd R α] (c : R) (a : αᵃᵒᵖ) : AddOpposite.unop (c +ᵥ a) = c +ᵥ AddOpposite.unop a

@[simp]

theorem MulOpposite.unop_smul {α : Type u_1} {R : Type u_2} [SMul R α] (c : R) (a : αᵐᵒᵖ) : MulOpposite.unop (c • a) = c • MulOpposite.unop a

@[simp]

theorem MulOpposite.unop_eq_zero_iff {α : Type u_1} [Zero α] (a : αᵐᵒᵖ) : MulOpposite.unop a = 0 ↔ a = 0

@[simp]

theorem MulOpposite.op_eq_zero_iff {α : Type u_1} [Zero α] (a : α) : MulOpposite.op a = 0 ↔ a = 0

theorem MulOpposite.unop_ne_zero_iff {α : Type u_1} [Zero α] (a : αᵐᵒᵖ) : MulOpposite.unop a ≠ 0 ↔ a ≠ 0

theorem MulOpposite.op_ne_zero_iff {α : Type u_1} [Zero α] (a : α) : MulOpposite.op a ≠ 0 ↔ a ≠ 0

@[simp]

theorem AddOpposite.unop_eq_zero_iff {α : Type u_1} [Zero α] (a : αᵃᵒᵖ) : AddOpposite.unop a = 0 ↔ a = 0

@[simp]

theorem MulOpposite.unop_eq_one_iff {α : Type u_1} [One α] (a : αᵐᵒᵖ) : MulOpposite.unop a = 1 ↔ a = 1

@[simp]

theorem AddOpposite.op_eq_zero_iff {α : Type u_1} [Zero α] (a : α) : AddOpposite.op a = 0 ↔ a = 0

@[simp]

theorem MulOpposite.op_eq_one_iff {α : Type u_1} [One α] (a : α) : MulOpposite.op a = 1 ↔ a = 1

instance AddOpposite.one {α : Type u_1} [One α] : One αᵃᵒᵖ

Equations

• AddOpposite.one = { one := AddOpposite.op 1 }

@[simp]

theorem AddOpposite.op_one {α : Type u_1} [One α] : AddOpposite.op 1 = 1

@[simp]

theorem AddOpposite.unop_one {α : Type u_1} [One α] : AddOpposite.unop 1 = 1

@[simp]

theorem AddOpposite.op_eq_one_iff {α : Type u_1} [One α] {a : α} : AddOpposite.op a = 1 ↔ a = 1

@[simp]

theorem AddOpposite.unop_eq_one_iff {α : Type u_1} [One α] {a : αᵃᵒᵖ} : AddOpposite.unop a = 1 ↔ a = 1

instance AddOpposite.mul {α : Type u_1} [Mul α] : Mul αᵃᵒᵖ

Equations

• AddOpposite.mul = { mul := fun (a b : αᵃᵒᵖ) => AddOpposite.op (AddOpposite.unop a * AddOpposite.unop b) }

@[simp]

theorem AddOpposite.op_mul {α : Type u_1} [Mul α] (a : α) (b : α) : AddOpposite.op (a * b) = AddOpposite.op a * AddOpposite.op b

@[simp]

theorem AddOpposite.unop_mul {α : Type u_1} [Mul α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : AddOpposite.unop (a * b) = AddOpposite.unop a * AddOpposite.unop b

instance AddOpposite.inv {α : Type u_1} [Inv α] : Inv αᵃᵒᵖ

Equations

• AddOpposite.inv = { inv := fun (a : αᵃᵒᵖ) => AddOpposite.op (AddOpposite.unop a)⁻¹ }

instance AddOpposite.involutiveInv {α : Type u_1} [InvolutiveInv α] : InvolutiveInv αᵃᵒᵖ

Equations

• AddOpposite.involutiveInv = let src := AddOpposite.inv; InvolutiveInv.mk (_ : ∀ (x : αᵃᵒᵖ), x⁻¹⁻¹ = x)

@[simp]

theorem AddOpposite.op_inv {α : Type u_1} [Inv α] (a : α) : AddOpposite.op a⁻¹ = (AddOpposite.op a)⁻¹

@[simp]

theorem AddOpposite.unop_inv {α : Type u_1} [Inv α] (a : αᵃᵒᵖ) : AddOpposite.unop a⁻¹ = (AddOpposite.unop a)⁻¹

instance AddOpposite.div {α : Type u_1} [Div α] : Div αᵃᵒᵖ

Equations

• AddOpposite.div = { div := fun (a b : αᵃᵒᵖ) => AddOpposite.op (AddOpposite.unop a / AddOpposite.unop b) }

@[simp]

theorem AddOpposite.op_div {α : Type u_1} [Div α] (a : α) (b : α) : AddOpposite.op (a / b) = AddOpposite.op a / AddOpposite.op b

@[simp]

theorem AddOpposite.unop_div {α : Type u_1} [Div α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) : AddOpposite.unop (a / b) = AddOpposite.unop a / AddOpposite.unop b