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 #

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 MulOpposite (α : 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.

Instances For
    structure AddOpposite (α : 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.

    Instances For

      Multiplicative opposite of a type.

      Equations

      Additive opposite of a type.

      Equations
      theorem AddOpposite.unop_op {α : Type u_1} (x : α) :
      { unop := x }.unop = x
      theorem MulOpposite.unop_op {α : Type u_1} (x : α) :
      { unop := x }.unop = x
      @[simp]
      theorem AddOpposite.op_unop {α : Type u_1} (x : αᵃᵒᵖ) :
      { unop := x.unop } = x
      @[simp]
      theorem MulOpposite.op_unop {α : Type u_1} (x : αᵐᵒᵖ) :
      { unop := x.unop } = 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 { unop := X }) (X : αᵃᵒᵖ) :
      F X

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

      Equations
      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
      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) }
      @[simp]
      theorem MulOpposite.opEquiv_symm_apply {α : Type u_1} :
      ↑(Equiv.symm MulOpposite.opEquiv) = MulOpposite.unop
      @[simp]
      theorem MulOpposite.opEquiv_apply {α : Type u_1} :
      MulOpposite.opEquiv = MulOpposite.op
      @[simp]
      theorem AddOpposite.opEquiv_apply {α : Type u_1} :
      AddOpposite.opEquiv = AddOpposite.op
      @[simp]
      theorem AddOpposite.opEquiv_symm_apply {α : Type u_1} :
      ↑(Equiv.symm AddOpposite.opEquiv) = AddOpposite.unop
      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) }
      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.unop_injective {α : Type u_1} :
      Function.Injective AddOpposite.unop
      theorem MulOpposite.unop_injective {α : Type u_1} :
      Function.Injective MulOpposite.unop
      theorem AddOpposite.op_inj {α : Type u_1} {x : α} {y : α} :
      { unop := x } = { unop := y } x = y
      theorem MulOpposite.op_inj {α : Type u_1} {x : α} {y : α} :
      { unop := x } = { unop := y } x = y
      @[simp]
      theorem AddOpposite.unop_inj {α : Type u_1} {x : αᵃᵒᵖ} {y : αᵃᵒᵖ} :
      x.unop = y.unop x = y
      @[simp]
      theorem MulOpposite.unop_inj {α : Type u_1} {x : αᵐᵒᵖ} {y : αᵐᵒᵖ} :
      x.unop = y.unop x = y
      instance AddOpposite.inhabited (α : Type u_1) [inst : Inhabited α] :
      Equations
      instance MulOpposite.inhabited (α : Type u_1) [inst : Inhabited α] :
      Equations
      instance MulOpposite.zero (α : Type u_1) [inst : Zero α] :
      Equations
      instance AddOpposite.zero (α : Type u_1) [inst : Zero α] :
      Equations
      instance MulOpposite.one (α : Type u_1) [inst : One α] :
      Equations
      instance MulOpposite.add (α : Type u_1) [inst : Add α] :
      Equations
      instance MulOpposite.sub (α : Type u_1) [inst : Sub α] :
      Equations
      instance MulOpposite.neg (α : Type u_1) [inst : Neg α] :
      Equations
      Equations
      instance AddOpposite.add (α : Type u_1) [inst : Add α] :
      Equations
      instance MulOpposite.mul (α : Type u_1) [inst : Mul α] :
      Equations
      instance AddOpposite.neg (α : Type u_1) [inst : Neg α] :
      Equations
      instance MulOpposite.inv (α : Type u_1) [inst : Inv α] :
      Equations
      def AddOpposite.involutiveNeg.proof_1 (α : Type u_1) [inst : InvolutiveNeg α] :
      ∀ (x : αᵃᵒᵖ), - -x = x
      Equations
      Equations
      instance AddOpposite.vadd (α : Type u_1) (R : Type u_2) [inst : VAdd R α] :
      Equations
      instance MulOpposite.smul (α : Type u_1) (R : Type u_2) [inst : SMul R α] :
      Equations
      @[simp]
      theorem MulOpposite.op_zero (α : Type u_1) [inst : Zero α] :
      { unop := 0 } = 0
      @[simp]
      theorem MulOpposite.unop_zero (α : Type u_1) [inst : Zero α] :
      0.unop = 0
      @[simp]
      theorem AddOpposite.op_zero (α : Type u_1) [inst : Zero α] :
      { unop := 0 } = 0
      @[simp]
      theorem MulOpposite.op_one (α : Type u_1) [inst : One α] :
      { unop := 1 } = 1
      @[simp]
      theorem AddOpposite.unop_zero (α : Type u_1) [inst : Zero α] :
      0.unop = 0
      @[simp]
      theorem MulOpposite.unop_one (α : Type u_1) [inst : One α] :
      1.unop = 1
      @[simp]
      theorem MulOpposite.op_add {α : Type u_1} [inst : Add α] (x : α) (y : α) :
      { unop := x + y } = { unop := x } + { unop := y }
      @[simp]
      theorem MulOpposite.unop_add {α : Type u_1} [inst : Add α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) :
      (x + y).unop = x.unop + y.unop
      @[simp]
      theorem MulOpposite.op_neg {α : Type u_1} [inst : Neg α] (x : α) :
      { unop := -x } = -{ unop := x }
      @[simp]
      theorem MulOpposite.unop_neg {α : Type u_1} [inst : Neg α] (x : αᵐᵒᵖ) :
      (-x).unop = -x.unop
      @[simp]
      theorem AddOpposite.op_add {α : Type u_1} [inst : Add α] (x : α) (y : α) :
      { unop := x + y } = { unop := y } + { unop := x }
      @[simp]
      theorem MulOpposite.op_mul {α : Type u_1} [inst : Mul α] (x : α) (y : α) :
      { unop := x * y } = { unop := y } * { unop := x }
      @[simp]
      theorem AddOpposite.unop_add {α : Type u_1} [inst : Add α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) :
      (x + y).unop = y.unop + x.unop
      @[simp]
      theorem MulOpposite.unop_mul {α : Type u_1} [inst : Mul α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) :
      (x * y).unop = y.unop * x.unop
      @[simp]
      theorem AddOpposite.op_neg {α : Type u_1} [inst : Neg α] (x : α) :
      { unop := -x } = -{ unop := x }
      @[simp]
      theorem MulOpposite.op_inv {α : Type u_1} [inst : Inv α] (x : α) :
      { unop := x⁻¹ } = { unop := x }⁻¹
      @[simp]
      theorem AddOpposite.unop_neg {α : Type u_1} [inst : Neg α] (x : αᵃᵒᵖ) :
      (-x).unop = -x.unop
      @[simp]
      theorem MulOpposite.unop_inv {α : Type u_1} [inst : Inv α] (x : αᵐᵒᵖ) :
      x⁻¹.unop = x.unop⁻¹
      @[simp]
      theorem MulOpposite.op_sub {α : Type u_1} [inst : Sub α] (x : α) (y : α) :
      { unop := x - y } = { unop := x } - { unop := y }
      @[simp]
      theorem MulOpposite.unop_sub {α : Type u_1} [inst : Sub α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) :
      (x - y).unop = x.unop - y.unop
      @[simp]
      theorem AddOpposite.op_vadd {α : Type u_2} {R : Type u_1} [inst : VAdd R α] (c : R) (a : α) :
      { unop := c +ᵥ a } = c +ᵥ { unop := a }
      @[simp]
      theorem MulOpposite.op_smul {α : Type u_2} {R : Type u_1} [inst : SMul R α] (c : R) (a : α) :
      { unop := c a } = c { unop := a }
      @[simp]
      theorem AddOpposite.unop_vadd {α : Type u_2} {R : Type u_1} [inst : VAdd R α] (c : R) (a : αᵃᵒᵖ) :
      (c +ᵥ a).unop = c +ᵥ a.unop
      @[simp]
      theorem MulOpposite.unop_smul {α : Type u_2} {R : Type u_1} [inst : SMul R α] (c : R) (a : αᵐᵒᵖ) :
      (c a).unop = c a.unop
      @[simp]
      theorem MulOpposite.unop_eq_zero_iff {α : Type u_1} [inst : Zero α] (a : αᵐᵒᵖ) :
      a.unop = 0 a = 0
      @[simp]
      theorem MulOpposite.op_eq_zero_iff {α : Type u_1} [inst : Zero α] (a : α) :
      { unop := a } = 0 a = 0
      theorem MulOpposite.unop_ne_zero_iff {α : Type u_1} [inst : Zero α] (a : αᵐᵒᵖ) :
      a.unop 0 a 0
      theorem MulOpposite.op_ne_zero_iff {α : Type u_1} [inst : Zero α] (a : α) :
      { unop := a } 0 a 0
      @[simp]
      theorem AddOpposite.unop_eq_zero_iff {α : Type u_1} [inst : Zero α] (a : αᵃᵒᵖ) :
      a.unop = 0 a = 0
      @[simp]
      theorem MulOpposite.unop_eq_one_iff {α : Type u_1} [inst : One α] (a : αᵐᵒᵖ) :
      a.unop = 1 a = 1
      @[simp]
      theorem AddOpposite.op_eq_zero_iff {α : Type u_1} [inst : Zero α] (a : α) :
      { unop := a } = 0 a = 0
      @[simp]
      theorem MulOpposite.op_eq_one_iff {α : Type u_1} [inst : One α] (a : α) :
      { unop := a } = 1 a = 1
      instance AddOpposite.one {α : Type u_1} [inst : One α] :
      Equations
      • AddOpposite.one = { one := { unop := 1 } }
      @[simp]
      theorem AddOpposite.op_one {α : Type u_1} [inst : One α] :
      { unop := 1 } = 1
      @[simp]
      theorem AddOpposite.unop_one {α : Type u_1} [inst : One α] :
      1.unop = 1
      @[simp]
      theorem AddOpposite.op_eq_one_iff {α : Type u_1} [inst : One α] {a : α} :
      { unop := a } = 1 a = 1
      @[simp]
      theorem AddOpposite.unop_eq_one_iff {α : Type u_1} [inst : One α] {a : αᵃᵒᵖ} :
      a.unop = 1 a = 1
      instance AddOpposite.mul {α : Type u_1} [inst : Mul α] :
      Equations
      • AddOpposite.mul = { mul := fun a b => { unop := a.unop * b.unop } }
      @[simp]
      theorem AddOpposite.op_mul {α : Type u_1} [inst : Mul α] (a : α) (b : α) :
      { unop := a * b } = { unop := a } * { unop := b }
      @[simp]
      theorem AddOpposite.unop_mul {α : Type u_1} [inst : Mul α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
      (a * b).unop = a.unop * b.unop
      instance AddOpposite.inv {α : Type u_1} [inst : Inv α] :
      Equations
      • AddOpposite.inv = { inv := fun a => { unop := a.unop⁻¹ } }
      Equations
      @[simp]
      theorem AddOpposite.op_inv {α : Type u_1} [inst : Inv α] (a : α) :
      { unop := a⁻¹ } = { unop := a }⁻¹
      @[simp]
      theorem AddOpposite.unop_inv {α : Type u_1} [inst : Inv α] (a : αᵃᵒᵖ) :
      a⁻¹.unop = a.unop⁻¹
      instance AddOpposite.div {α : Type u_1} [inst : Div α] :
      Equations
      • AddOpposite.div = { div := fun a b => { unop := a.unop / b.unop } }
      @[simp]
      theorem AddOpposite.op_div {α : Type u_1} [inst : Div α] (a : α) (b : α) :
      { unop := a / b } = { unop := a } / { unop := b }
      @[simp]
      theorem AddOpposite.unop_div {α : Type u_1} [inst : Div α] (a : αᵃᵒᵖ) (b : αᵃᵒᵖ) :
      (a / b).unop = a.unop / b.unop