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 #

multiplicative opposite, additive opposite

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 https://github.com/leanprover-community/mathlib4/pull/1036).

op' :: (

unop' : α
The element of α represented by x : PreOpposite α.

)

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

αᵐᵒᵖ = 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

αᵃᵒᵖ = PreOpposite α

Instances For

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 MulOpposite.op {α : Type u_1} :

α → αᵐᵒᵖ

The element of MulOpposite α that represents x : α.

Equations

MulOpposite.op = PreOpposite.op'

def AddOpposite.op {α : Type u_1} :

α → αᵃᵒᵖ

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

Equations

AddOpposite.op = PreOpposite.op'

def MulOpposite.unop {α : Type u_1} :

αᵐᵒᵖ → α

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

Equations

MulOpposite.unop = PreOpposite.unop'

def AddOpposite.unop {α : Type u_1} :

αᵃᵒᵖ → α

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

Equations

AddOpposite.unop = PreOpposite.unop'

@[simp]

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

unop (op x) = x

@[simp]

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

unop (op x) = x

@[simp]

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

op (unop x) = x

@[simp]

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

op (unop x) = x

@[simp]

theorem MulOpposite.op_comp_unop {α : Type u_1} :

op ∘ unop = id

@[simp]

theorem AddOpposite.op_comp_unop {α : Type u_1} :

op ∘ unop = id

@[simp]

theorem MulOpposite.unop_comp_op {α : Type u_1} :

unop ∘ op = id

@[simp]

theorem AddOpposite.unop_comp_op {α : Type u_1} :

unop ∘ op = id

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

F X

A recursor for MulOpposite. Use as induction x.

Equations

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

def AddOpposite.rec' {α : Type u_1} {F : αᵃᵒᵖ → Sort u_3} (h : (X : α) → F (op X)) (X : αᵃᵒᵖ) :

F X

A recursor for AddOpposite. Use as induction x.

Equations

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

def MulOpposite.opEquiv {α : Type u_1} :

α ≃ αᵐᵒᵖ

The canonical bijection between α and αᵐᵒᵖ.

Equations

MulOpposite.opEquiv = { toFun := MulOpposite.op, invFun := MulOpposite.unop, left_inv := ⋯, right_inv := ⋯ }

def AddOpposite.opEquiv {α : Type u_1} :

α ≃ αᵃᵒᵖ

The canonical bijection between α and αᵃᵒᵖ.

Equations

AddOpposite.opEquiv = { toFun := AddOpposite.op, invFun := AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MulOpposite.opEquiv_apply {α : Type u_1} :

⇑opEquiv = op

@[simp]

theorem AddOpposite.opEquiv_apply {α : Type u_1} :

⇑opEquiv = op

@[simp]

theorem MulOpposite.opEquiv_symm_apply {α : Type u_1} :

⇑opEquiv.symm = unop

@[simp]

theorem AddOpposite.opEquiv_symm_apply {α : Type u_1} :

⇑opEquiv.symm = unop

theorem MulOpposite.op_bijective {α : Type u_1} :

Function.Bijective op

theorem AddOpposite.op_bijective {α : Type u_1} :

Function.Bijective op

theorem MulOpposite.unop_bijective {α : Type u_1} :

Function.Bijective unop

theorem AddOpposite.unop_bijective {α : Type u_1} :

Function.Bijective unop

theorem MulOpposite.op_injective {α : Type u_1} :

Function.Injective op

theorem AddOpposite.op_injective {α : Type u_1} :

Function.Injective op

theorem MulOpposite.op_surjective {α : Type u_1} :

Function.Surjective op

theorem AddOpposite.op_surjective {α : Type u_1} :

Function.Surjective op

theorem MulOpposite.unop_injective {α : Type u_1} :

Function.Injective unop

theorem AddOpposite.unop_injective {α : Type u_1} :

Function.Injective unop

theorem MulOpposite.unop_surjective {α : Type u_1} :

Function.Surjective unop

theorem AddOpposite.unop_surjective {α : Type u_1} :

Function.Surjective unop

@[simp]

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

op x = op y ↔ x = y

@[simp]

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

op x = op y ↔ x = y

@[simp]

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

unop x = unop y ↔ x = y

@[simp]

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

unop x = unop y ↔ x = y

@[simp]

theorem MulOpposite.forall {α : Type u_1} {p : αᵐᵒᵖ → Prop} :

(∀ (a : αᵐᵒᵖ), p a) ↔ ∀ (a : α), p (op a)

@[simp]

theorem AddOpposite.forall {α : Type u_1} {p : αᵃᵒᵖ → Prop} :

(∀ (a : αᵃᵒᵖ), p a) ↔ ∀ (a : α), p (op a)

@[simp]

theorem MulOpposite.exists {α : Type u_1} {p : αᵐᵒᵖ → Prop} :

(∃ (a : αᵐᵒᵖ ), p a) ↔ ∃ (a : α), p (op a)

@[simp]

theorem AddOpposite.exists {α : Type u_1} {p : αᵃᵒᵖ → Prop} :

(∃ (a : αᵃᵒᵖ ), p a) ↔ ∃ (a : α), p (op a)

instance MulOpposite.instNontrivial {α : Type u_1} [Nontrivial α] :

Nontrivial αᵐᵒᵖ

instance AddOpposite.instNontrivial {α : Type u_1} [Nontrivial α] :

Nontrivial αᵃᵒᵖ

instance MulOpposite.instInhabited {α : Type u_1} [Inhabited α] :

Inhabited αᵐᵒᵖ

Equations

MulOpposite.instInhabited = { default := MulOpposite.op default }

instance AddOpposite.instInhabited {α : Type u_1} [Inhabited α] :

Inhabited αᵃᵒᵖ

Equations

AddOpposite.instInhabited = { default := AddOpposite.op default }

instance MulOpposite.instSubsingleton {α : Type u_1} [Subsingleton α] :

Subsingleton αᵐᵒᵖ

instance AddOpposite.instSubsingleton {α : Type u_1} [Subsingleton α] :

Subsingleton αᵃᵒᵖ

instance MulOpposite.instUnique {α : Type u_1} [Unique α] :

Unique αᵐᵒᵖ

Equations

MulOpposite.instUnique = Unique.mk' αᵐᵒᵖ

instance AddOpposite.instUnique {α : Type u_1} [Unique α] :

Unique αᵃᵒᵖ

Equations

AddOpposite.instUnique = Unique.mk' αᵃᵒᵖ

instance MulOpposite.instIsEmpty {α : Type u_1} [IsEmpty α] :

IsEmpty αᵐᵒᵖ

instance AddOpposite.instIsEmpty {α : Type u_1} [IsEmpty α] :

IsEmpty αᵃᵒᵖ

instance MulOpposite.instDecidableEq {α : Type u_1} [DecidableEq α] :

DecidableEq αᵐᵒᵖ

Equations

MulOpposite.instDecidableEq = ⋯.decidableEq

instance AddOpposite.instDecidableEq {α : Type u_1} [DecidableEq α] :

DecidableEq αᵃᵒᵖ

Equations

AddOpposite.instDecidableEq = ⋯.decidableEq

instance MulOpposite.instZero {α : Type u_1} [Zero α] :

Zero αᵐᵒᵖ

Equations

MulOpposite.instZero = { zero := MulOpposite.op 0 }

instance MulOpposite.instOne {α : Type u_1} [One α] :

One αᵐᵒᵖ

Equations

MulOpposite.instOne = { one := MulOpposite.op 1 }

instance AddOpposite.instZero {α : Type u_1} [Zero α] :

Zero αᵃᵒᵖ

Equations

AddOpposite.instZero = { zero := AddOpposite.op 0 }

instance MulOpposite.instAdd {α : Type u_1} [Add α] :

Add αᵐᵒᵖ

Equations

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

instance MulOpposite.instSub {α : Type u_1} [Sub α] :

Sub αᵐᵒᵖ

Equations

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

instance MulOpposite.instNeg {α : Type u_1} [Neg α] :

Neg αᵐᵒᵖ

Equations

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

instance MulOpposite.instInvolutiveNeg {α : Type u_1} [InvolutiveNeg α] :

InvolutiveNeg αᵐᵒᵖ

Equations

MulOpposite.instInvolutiveNeg = InvolutiveNeg.mk ⋯

instance MulOpposite.instMul {α : Type u_1} [Mul α] :

Mul αᵐᵒᵖ

Equations

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

instance AddOpposite.instAdd {α : Type u_1} [Add α] :

Add αᵃᵒᵖ

Equations

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

instance MulOpposite.instInv {α : Type u_1} [Inv α] :

Inv αᵐᵒᵖ

Equations

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

instance AddOpposite.instNeg {α : Type u_1} [Neg α] :

Neg αᵃᵒᵖ

Equations

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

instance MulOpposite.instInvolutiveInv {α : Type u_1} [InvolutiveInv α] :

InvolutiveInv αᵐᵒᵖ

Equations

MulOpposite.instInvolutiveInv = InvolutiveInv.mk ⋯

instance AddOpposite.instInvolutiveNeg {α : Type u_1} [InvolutiveNeg α] :

InvolutiveNeg αᵃᵒᵖ

Equations

AddOpposite.instInvolutiveNeg = InvolutiveNeg.mk ⋯

instance MulOpposite.instSMul {α : Type u_1} {β : Type u_2} [SMul α β] :

SMul α βᵐᵒᵖ

Equations

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

instance AddOpposite.instVAdd {α : Type u_1} {β : Type u_2} [VAdd α β] :

VAdd α βᵃᵒᵖ

Equations

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

@[simp]

theorem MulOpposite.op_zero {α : Type u_1} [Zero α] :

op 0 = 0

@[simp]

theorem MulOpposite.unop_zero {α : Type u_1} [Zero α] :

unop 0 = 0

@[simp]

theorem MulOpposite.op_one {α : Type u_1} [One α] :

op 1 = 1

@[simp]

theorem AddOpposite.op_zero {α : Type u_1} [Zero α] :

op 0 = 0

@[simp]

theorem MulOpposite.unop_one {α : Type u_1} [One α] :

unop 1 = 1

@[simp]

theorem AddOpposite.unop_zero {α : Type u_1} [Zero α] :

unop 0 = 0

@[simp]

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

op (x + y) = op x + op y

@[simp]

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

unop (x + y) = unop x + unop y

@[simp]

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

op (-x) = -op x

@[simp]

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

unop (-x) = -unop x

@[simp]

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

op (x * y) = op y * op x

@[simp]

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

op (x + y) = op y + op x

@[simp]

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

unop (x * y) = unop y * unop x

@[simp]

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

unop (x + y) = unop y + unop x

@[simp]

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

op x⁻¹ = (op x)⁻¹

@[simp]

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

op (-x) = -op x

@[simp]

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

unop x⁻¹ = (unop x)⁻¹

@[simp]

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

unop (-x) = -unop x

@[simp]

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

op (x - y) = op x - op y

@[simp]

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

unop (x - y) = unop x - unop y

@[simp]

theorem MulOpposite.op_smul {α : Type u_1} {β : Type u_2} [SMul α β] (a : α) (b : β) :

op (a • b) = a • op b

@[simp]

theorem AddOpposite.op_vadd {α : Type u_1} {β : Type u_2} [VAdd α β] (a : α) (b : β) :

op (a +ᵥ b) = a +ᵥ op b

@[simp]

theorem MulOpposite.unop_smul {α : Type u_1} {β : Type u_2} [SMul α β] (a : α) (b : βᵐᵒᵖ) :

unop (a • b) = a • unop b

@[simp]

theorem AddOpposite.unop_vadd {α : Type u_1} {β : Type u_2} [VAdd α β] (a : α) (b : βᵃᵒᵖ) :

unop (a +ᵥ b) = a +ᵥ unop b

@[simp]

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

unop a = 0 ↔ a = 0

@[simp]

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

op a = 0 ↔ a = 0

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

unop a ≠ 0 ↔ a ≠ 0

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

op a ≠ 0 ↔ a ≠ 0

@[simp]

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

unop a = 1 ↔ a = 1

@[simp]

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

unop a = 0 ↔ a = 0

@[simp]

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

op a = 1 ↔ a = 1

@[simp]

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

op a = 0 ↔ a = 0

instance AddOpposite.instOne {α : Type u_1} [One α] :

One αᵃᵒᵖ

Equations

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

@[simp]

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

op 1 = 1

@[simp]

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

unop 1 = 1

@[simp]

theorem AddOpposite.op_eq_one_iff {α : Type u_1} [One α] {a : α} :

op a = 1 ↔ a = 1

@[simp]

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

unop a = 1 ↔ a = 1

instance AddOpposite.instMul {α : Type u_1} [Mul α] :

Mul αᵃᵒᵖ

Equations

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

@[simp]

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

op (a * b) = op a * op b

@[simp]

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

unop (a * b) = unop a * unop b

instance AddOpposite.instInv {α : Type u_1} [Inv α] :

Inv αᵃᵒᵖ

Equations

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

instance AddOpposite.instInvolutiveInv {α : Type u_1} [InvolutiveInv α] :

InvolutiveInv αᵃᵒᵖ

Equations

AddOpposite.instInvolutiveInv = InvolutiveInv.mk ⋯

@[simp]

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

op a⁻¹ = (op a)⁻¹

@[simp]

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

unop a⁻¹ = (unop a)⁻¹

instance AddOpposite.instDiv {α : Type u_1} [Div α] :

Div αᵃᵒᵖ

Equations

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

@[simp]

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

op (a / b) = op a / op b

@[simp]

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

unop (a / b) = unop a / unop b