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

  • )
Instances For
    def AddOpposite (α : Type u) :

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

    Equations
    Instances For
      def MulOpposite (α : Type u) :

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

      Equations
      Instances For

        Multiplicative opposite of a type.

        Equations
        Instances For

          Additive opposite of a type.

          Equations
          Instances For
            def AddOpposite.op {α : Type u_1} :
            ααᵃᵒᵖ

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

            Equations
            • AddOpposite.op = PreOpposite.op'
            Instances For
              def MulOpposite.op {α : Type u_1} :
              ααᵐᵒᵖ

              The element of MulOpposite α that represents x : α.

              Equations
              • MulOpposite.op = PreOpposite.op'
              Instances For
                def AddOpposite.unop {α : Type u_1} :
                αᵃᵒᵖα

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

                Equations
                • AddOpposite.unop = PreOpposite.unop'
                Instances For
                  def MulOpposite.unop {α : Type u_1} :
                  αᵐᵒᵖα

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

                  Equations
                  • MulOpposite.unop = PreOpposite.unop'
                  Instances For
                    @[simp]
                    theorem AddOpposite.unop_op {α : Type u_1} (x : α) :
                    @[simp]
                    theorem MulOpposite.unop_op {α : Type u_1} (x : α) :
                    @[simp]
                    @[simp]
                    @[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
                    Instances For
                      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
                      Instances For
                        def AddOpposite.opEquiv {α : Type u_1} :

                        The canonical bijection between α and αᵃᵒᵖ.

                        Equations
                        • AddOpposite.opEquiv = { toFun := AddOpposite.op, invFun := AddOpposite.unop, left_inv := , right_inv := }
                        Instances For
                          @[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
                          • MulOpposite.opEquiv = { toFun := MulOpposite.op, invFun := MulOpposite.unop, left_inv := , right_inv := }
                          Instances For
                            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 : α} :
                            @[simp]
                            theorem MulOpposite.op_inj {α : Type u_1} {x : α} {y : α} :
                            @[simp]
                            @[simp]
                            Equations
                            • =
                            Equations
                            • =
                            Equations
                            Equations
                            Equations
                            • =
                            Equations
                            • =
                            instance AddOpposite.isEmpty (α : Type u_1) [IsEmpty α] :
                            Equations
                            • =
                            instance MulOpposite.isEmpty (α : Type u_1) [IsEmpty α] :
                            Equations
                            • =
                            instance MulOpposite.zero (α : Type u_1) [Zero α] :
                            Equations
                            instance AddOpposite.zero (α : Type u_1) [Zero α] :
                            Equations
                            instance MulOpposite.one (α : Type u_1) [One α] :
                            Equations
                            instance MulOpposite.add (α : Type u_1) [Add α] :
                            Equations
                            instance MulOpposite.sub (α : Type u_1) [Sub α] :
                            Equations
                            instance MulOpposite.neg (α : Type u_1) [Neg α] :
                            Equations
                            instance AddOpposite.add (α : Type u_1) [Add α] :
                            Equations
                            instance MulOpposite.mul (α : Type u_1) [Mul α] :
                            Equations
                            instance AddOpposite.neg (α : Type u_1) [Neg α] :
                            Equations
                            instance MulOpposite.inv (α : Type u_1) [Inv α] :
                            Equations
                            theorem AddOpposite.involutiveNeg.proof_1 (α : Type u_1) [InvolutiveNeg α] :
                            ∀ (x : αᵃᵒᵖ), - -x = x
                            instance AddOpposite.vadd (α : Type u_1) (R : Type u_2) [VAdd R α] :
                            Equations
                            instance MulOpposite.smul (α : Type u_1) (R : Type u_2) [SMul R α] :
                            Equations
                            @[simp]
                            theorem MulOpposite.op_zero (α : Type u_1) [Zero α] :
                            @[simp]
                            theorem MulOpposite.unop_zero (α : Type u_1) [Zero α] :
                            @[simp]
                            theorem AddOpposite.op_zero (α : Type u_1) [Zero α] :
                            @[simp]
                            theorem MulOpposite.op_one (α : Type u_1) [One α] :
                            @[simp]
                            theorem AddOpposite.unop_zero (α : Type u_1) [Zero α] :
                            @[simp]
                            theorem MulOpposite.unop_one (α : Type u_1) [One α] :
                            @[simp]
                            theorem MulOpposite.op_add {α : Type u_1} [Add α] (x : α) (y : α) :
                            @[simp]
                            @[simp]
                            theorem MulOpposite.op_neg {α : Type u_1} [Neg α] (x : α) :
                            @[simp]
                            @[simp]
                            theorem AddOpposite.op_add {α : Type u_1} [Add α] (x : α) (y : α) :
                            @[simp]
                            theorem MulOpposite.op_mul {α : Type u_1} [Mul α] (x : α) (y : α) :
                            @[simp]
                            @[simp]
                            @[simp]
                            theorem AddOpposite.op_neg {α : Type u_1} [Neg α] (x : α) :
                            @[simp]
                            theorem MulOpposite.op_inv {α : Type u_1} [Inv α] (x : α) :
                            @[simp]
                            @[simp]
                            theorem MulOpposite.op_sub {α : Type u_1} [Sub α] (x : α) (y : α) :
                            @[simp]
                            @[simp]
                            theorem AddOpposite.op_vadd {α : Type u_1} {R : Type u_2} [VAdd R α] (c : R) (a : α) :
                            @[simp]
                            theorem MulOpposite.op_smul {α : Type u_1} {R : Type u_2} [SMul R α] (c : R) (a : α) :
                            @[simp]
                            theorem AddOpposite.unop_vadd {α : Type u_1} {R : Type u_2} [VAdd R α] (c : R) (a : αᵃᵒᵖ) :
                            @[simp]
                            theorem MulOpposite.unop_smul {α : Type u_1} {R : Type u_2} [SMul R α] (c : R) (a : αᵐᵒᵖ) :
                            @[simp]
                            theorem MulOpposite.unop_eq_zero_iff {α : Type u_1} [Zero α] (a : αᵐᵒᵖ) :
                            @[simp]
                            theorem MulOpposite.op_eq_zero_iff {α : Type u_1} [Zero α] (a : α) :
                            theorem MulOpposite.op_ne_zero_iff {α : Type u_1} [Zero α] (a : α) :
                            @[simp]
                            theorem AddOpposite.unop_eq_zero_iff {α : Type u_1} [Zero α] (a : αᵃᵒᵖ) :
                            @[simp]
                            theorem MulOpposite.unop_eq_one_iff {α : Type u_1} [One α] (a : αᵐᵒᵖ) :
                            @[simp]
                            theorem AddOpposite.op_eq_zero_iff {α : Type u_1} [Zero α] (a : α) :
                            @[simp]
                            theorem MulOpposite.op_eq_one_iff {α : Type u_1} [One α] (a : α) :
                            instance AddOpposite.one {α : Type u_1} [One α] :
                            Equations
                            @[simp]
                            theorem AddOpposite.op_one {α : Type u_1} [One α] :
                            @[simp]
                            theorem AddOpposite.unop_one {α : Type u_1} [One α] :
                            @[simp]
                            theorem AddOpposite.op_eq_one_iff {α : Type u_1} [One α] {a : α} :
                            @[simp]
                            theorem AddOpposite.unop_eq_one_iff {α : Type u_1} [One α] {a : αᵃᵒᵖ} :
                            instance AddOpposite.mul {α : Type u_1} [Mul α] :
                            Equations
                            @[simp]
                            theorem AddOpposite.op_mul {α : Type u_1} [Mul α] (a : α) (b : α) :
                            @[simp]
                            instance AddOpposite.inv {α : Type u_1} [Inv α] :
                            Equations
                            Equations
                            @[simp]
                            theorem AddOpposite.op_inv {α : Type u_1} [Inv α] (a : α) :
                            instance AddOpposite.div {α : Type u_1} [Div α] :
                            Equations
                            @[simp]
                            theorem AddOpposite.op_div {α : Type u_1} [Div α] (a : α) (b : α) :
                            @[simp]