Documentation

Mathlib.Algebra.Field.Opposite

Field structure on the multiplicative/additive opposite #

Equations
Equations
Equations
Equations
@[simp]
theorem AddOpposite.op_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
AddOpposite.op q = q
@[simp]
theorem MulOpposite.op_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
MulOpposite.op q = q
@[simp]
theorem AddOpposite.unop_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
@[simp]
theorem MulOpposite.unop_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
@[simp]
theorem AddOpposite.op_ratCast {α : Type u_1} [RatCast α] (q : ) :
AddOpposite.op q = q
@[simp]
theorem MulOpposite.op_ratCast {α : Type u_1} [RatCast α] (q : ) :
MulOpposite.op q = q
@[simp]
theorem AddOpposite.unop_ratCast {α : Type u_1} [RatCast α] (q : ) :
@[simp]
theorem MulOpposite.unop_ratCast {α : Type u_1} [RatCast α] (q : ) :
Equations
Equations
  • MulOpposite.instDivisionRing = DivisionRing.mk DivisionSemiring.zpow DivisionSemiring.nnqsmul (fun (q : ) => HMul.hMul q)
Equations
  • MulOpposite.instSemifield = Semifield.mk DivisionSemiring.zpow DivisionSemiring.nnqsmul
instance MulOpposite.instField {α : Type u_1} [Field α] :
Equations
  • MulOpposite.instField = Field.mk DivisionRing.zpow DivisionRing.nnqsmul DivisionRing.qsmul
Equations
Equations
  • AddOpposite.instDivisionRing = DivisionRing.mk DivisionSemiring.zpow DivisionSemiring.nnqsmul (fun (q : ) => HMul.hMul q)
Equations
  • AddOpposite.instSemifield = Semifield.mk DivisionSemiring.zpow DivisionSemiring.nnqsmul
instance AddOpposite.instField {α : Type u_1} [Field α] :
Equations
  • AddOpposite.instField = Field.mk DivisionRing.zpow DivisionRing.nnqsmul DivisionRing.qsmul