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.

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.

def «term_ᵐᵒᵖ» : Lean.TrailingParserDescr

Multiplicative opposite of a type.

def «term_ᵃᵒᵖ» : Lean.TrailingParserDescr

Additive opposite of a type.

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

The element of MulOpposite α that represents x : α.

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

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

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

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

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

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

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

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.

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

The canonical bijection between α and αᵐᵒᵖ.

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

The canonical bijection between α and αᵃᵒᵖ.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[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 αᵃᵒᵖ

@[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 αᵃᵒᵖ

@[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 αᵃᵒᵖ

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

@[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 αᵃᵒᵖ

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