# Field structure on the multiplicative/additive opposite #

instance AddOpposite.instNNRatCast {α : Type u_1} [] :
Equations
• AddOpposite.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => }
instance MulOpposite.instNNRatCast {α : Type u_1} [] :
Equations
• MulOpposite.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => }
instance AddOpposite.instRatCast {α : Type u_1} [] :
Equations
• AddOpposite.instRatCast = { ratCast := fun (q : ) => }
instance MulOpposite.instRatCast {α : Type u_1} [] :
Equations
• MulOpposite.instRatCast = { ratCast := fun (q : ) => }
@[simp]
theorem AddOpposite.op_nnratCast {α : Type u_1} [] (q : ℚ≥0) :
= q
@[simp]
theorem MulOpposite.op_nnratCast {α : Type u_1} [] (q : ℚ≥0) :
= q
@[simp]
theorem AddOpposite.unop_nnratCast {α : Type u_1} [] (q : ℚ≥0) :
(q).unop = q
@[simp]
theorem MulOpposite.unop_nnratCast {α : Type u_1} [] (q : ℚ≥0) :
(q).unop = q
@[simp]
theorem AddOpposite.op_ratCast {α : Type u_1} [] (q : ) :
= q
@[simp]
theorem MulOpposite.op_ratCast {α : Type u_1} [] (q : ) :
= q
@[simp]
theorem AddOpposite.unop_ratCast {α : Type u_1} [] (q : ) :
(q).unop = q
@[simp]
theorem MulOpposite.unop_ratCast {α : Type u_1} [] (q : ) :
(q).unop = q
instance MulOpposite.instDivisionSemiring {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
instance MulOpposite.instDivisionRing {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
instance MulOpposite.instSemifield {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
instance MulOpposite.instField {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.instDivisionSemiring {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.instDivisionRing {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.instSemifield {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.instField {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.