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

ink

structure MulOpposite (α : Type u) : 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.

ink

structure AddOpposite (α : Type u) : 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.

ink

def «term_ᵐᵒᵖ» : Lean.TrailingParserDescr

Multiplicative opposite of a type.

Equations

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

ink

def «term_ᵃᵒᵖ» : Lean.TrailingParserDescr

Additive opposite of a type.

Equations

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

ink

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

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

ink

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) }

ink

@[simp]

theorem MulOpposite.opEquiv_symm_apply {α : Type u_1} : ↑(Equiv.symm MulOpposite.opEquiv) = MulOpposite.unop

ink

@[simp]

theorem MulOpposite.opEquiv_apply {α : Type u_1} : ↑MulOpposite.opEquiv = MulOpposite.op

ink

@[simp]

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

ink

@[simp]

theorem AddOpposite.opEquiv_symm_apply {α : Type u_1} : ↑(Equiv.symm AddOpposite.opEquiv) = AddOpposite.unop

ink

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) }

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

def AddOpposite.nontrivial.proof_1 (α : Type u_1) [inst : Nontrivial α] : Nontrivial αᵃᵒᵖ

Equations

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

ink

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

Equations

• AddOpposite.nontrivial = AddOpposite.nontrivial.proof_1

ink

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

Equations

• MulOpposite.nontrivial = MulOpposite.nontrivial.proof_1

ink

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

Equations

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

ink

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

Equations

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

ink

def AddOpposite.subsingleton.proof_1 (α : Type u_1) [inst : Subsingleton α] : Subsingleton αᵃᵒᵖ

Equations

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

ink

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

Equations

• AddOpposite.subsingleton = AddOpposite.subsingleton.proof_1

ink

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

Equations

• MulOpposite.subsingleton = MulOpposite.subsingleton.proof_1

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

def AddOpposite.isEmpty.proof_1 (α : Type u_1) [inst : IsEmpty α] : IsEmpty αᵃᵒᵖ

Equations

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

ink

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

Equations

• AddOpposite.isEmpty = AddOpposite.isEmpty.proof_1

ink

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

Equations

• MulOpposite.isEmpty = MulOpposite.isEmpty.proof_1

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• MulOpposite.add α = { add := fun x y => { unop := x.unop + y.unop } }

ink

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

Equations

• MulOpposite.sub α = { sub := fun x y => { unop := x.unop - y.unop } }

ink

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

Equations

• MulOpposite.neg α = { neg := fun x => { unop := -x.unop } }

ink

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

Equations

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

ink

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

Equations

• AddOpposite.add α = { add := fun x y => { unop := y.unop + x.unop } }

ink

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

Equations

• MulOpposite.mul α = { mul := fun x y => { unop := y.unop * x.unop } }

ink

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

Equations

• AddOpposite.neg α = { neg := fun x => { unop := -x.unop } }

ink

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

Equations

• MulOpposite.inv α = { inv := fun x => { unop := x.unop⁻¹ } }

ink

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

Equations

• (_ : - -x = x) = (_ : - -x = x)

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• AddOpposite.vadd α R = { vadd := fun c x => { unop := c +ᵥ x.unop } }

ink

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

Equations

• MulOpposite.smul α R = { smul := fun c x => { unop := c • x.unop } }

ink

@[simp]

theorem MulOpposite.op_zero (α : Type u_1) [inst : Zero α] : { unop := 0 } = 0

ink

@[simp]

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

ink

@[simp]

theorem AddOpposite.op_zero (α : Type u_1) [inst : Zero α] : { unop := 0 } = 0

ink

@[simp]

theorem MulOpposite.op_one (α : Type u_1) [inst : One α] : { unop := 1 } = 1

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

• AddOpposite.mul = { mul := fun a b => { unop := a.unop * b.unop } }

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

• AddOpposite.inv = { inv := fun a => { unop := a.unop⁻¹ } }

ink

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

• AddOpposite.div = { div := fun a b => { unop := a.unop / b.unop } }

ink

@[simp]

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

ink

@[simp]

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