Documentation

Mathlib.Algebra.Field.Opposite

Field structure on the multiplicative/additive opposite #

source
instance MulOpposite.instNNRatCast {α : Type u_1} [NNRatCast α] :
NNRatCast αᵐᵒᵖ
Equations
    source
    instance AddOpposite.instNNRatCast {α : Type u_1} [NNRatCast α] :
    NNRatCast αᵃᵒᵖ
    Equations
      source
      instance MulOpposite.instRatCast {α : Type u_1} [RatCast α] :
      RatCast αᵐᵒᵖ
      Equations
        source
        instance AddOpposite.instRatCast {α : Type u_1} [RatCast α] :
        RatCast αᵃᵒᵖ
        Equations
          source
          @[simp]
          theorem MulOpposite.op_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
          op ↑q = ↑q
          source
          @[simp]
          theorem AddOpposite.op_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
          op ↑q = ↑q
          source
          @[simp]
          theorem MulOpposite.unop_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
          unop ↑q = ↑q
          source
          @[simp]
          theorem AddOpposite.unop_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
          unop ↑q = ↑q
          source
          @[simp]
          theorem MulOpposite.op_ratCast {α : Type u_1} [RatCast α] (q : ℚ) :
          op ↑q = ↑q
          source
          @[simp]
          theorem AddOpposite.op_ratCast {α : Type u_1} [RatCast α] (q : ℚ) :
          op ↑q = ↑q
          source
          @[simp]
          theorem MulOpposite.unop_ratCast {α : Type u_1} [RatCast α] (q : ℚ) :
          unop ↑q = ↑q
          source
          @[simp]
          theorem AddOpposite.unop_ratCast {α : Type u_1} [RatCast α] (q : ℚ) :
          unop ↑q = ↑q
          source
          instance MulOpposite.instDivisionSemiring {α : Type u_1} [DivisionSemiring α] :
          DivisionSemiring αᵐᵒᵖ
          Equations
            source
            instance MulOpposite.instDivisionRing {α : Type u_1} [DivisionRing α] :
            DivisionRing αᵐᵒᵖ
            Equations
              source
              instance MulOpposite.instSemifield {α : Type u_1} [Semifield α] :
              Semifield αᵐᵒᵖ
              Equations
                source
                instance MulOpposite.instField {α : Type u_1} [Field α] :
                Field αᵐᵒᵖ
                Equations
                  source
                  instance AddOpposite.instDivisionSemiring {α : Type u_1} [DivisionSemiring α] :
                  DivisionSemiring αᵃᵒᵖ
                  Equations
                    source
                    instance AddOpposite.instDivisionRing {α : Type u_1} [DivisionRing α] :
                    DivisionRing αᵃᵒᵖ
                    Equations
                      source
                      instance AddOpposite.instSemifield {α : Type u_1} [Semifield α] :
                      Semifield αᵃᵒᵖ
                      Equations
                        source
                        instance AddOpposite.instField {α : Type u_1} [Field α] :
                        Field αᵃᵒᵖ
                        Equations