Field structure on the multiplicative/additive opposite

instance AddOpposite.ratCast (α : Type u_1) [RatCast α] : RatCast αᵃᵒᵖ

instance MulOpposite.ratCast (α : Type u_1) [RatCast α] : RatCast αᵐᵒᵖ

@[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 : ℚ) : AddOpposite.unop ↑q = ↑q

@[simp]

theorem MulOpposite.unop_ratCast {α : Type u_1} [RatCast α] (q : ℚ) : MulOpposite.unop ↑q = ↑q

instance MulOpposite.divisionSemiring (α : Type u_1) [DivisionSemiring α] : DivisionSemiring αᵐᵒᵖ

instance MulOpposite.divisionRing (α : Type u_1) [DivisionRing α] : DivisionRing αᵐᵒᵖ

instance MulOpposite.semifield (α : Type u_1) [Semifield α] : Semifield αᵐᵒᵖ

instance MulOpposite.field (α : Type u_1) [Field α] : Field αᵐᵒᵖ

instance AddOpposite.divisionSemiring {α : Type u_1} [DivisionSemiring α] : DivisionSemiring αᵃᵒᵖ

instance AddOpposite.divisionRing {α : Type u_1} [DivisionRing α] : DivisionRing αᵃᵒᵖ

instance AddOpposite.semifield {α : Type u_1} [Semifield α] : Semifield αᵃᵒᵖ

instance AddOpposite.field {α : Type u_1} [Field α] : Field αᵃᵒᵖ