Field structure on the multiplicative/additive opposite

@[implicit_reducible]

instance MulOpposite.instNNRatCast {α : Type u_1} [NNRatCast α] : NNRatCast αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instNNRatCast {α : Type u_1} [NNRatCast α] : NNRatCast αᵃᵒᵖ

@[implicit_reducible]

instance MulOpposite.instRatCast {α : Type u_1} [RatCast α] : RatCast αᵐᵒᵖ

@[implicit_reducible]

instance AddOpposite.instRatCast {α : Type u_1} [RatCast α] : RatCast αᵃᵒᵖ

@[simp]

theorem MulOpposite.op_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) : op ↑q = ↑q

@[simp]

theorem AddOpposite.op_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) : op ↑q = ↑q

@[simp]

theorem MulOpposite.unop_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) : unop ↑q = ↑q

@[simp]

theorem AddOpposite.unop_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) : unop ↑q = ↑q

@[simp]

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

@[simp]

theorem AddOpposite.op_ratCast {α : Type u_1} [RatCast α] (q : ℚ) : op ↑q = ↑q

@[simp]

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

@[simp]

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

@[implicit_reducible]

instance MulOpposite.instDivisionSemiring {α : Type u_1} [DivisionSemiring α] : DivisionSemiring αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instDivisionRing {α : Type u_1} [DivisionRing α] : DivisionRing αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instSemifield {α : Type u_1} [Semifield α] : Semifield αᵐᵒᵖ

@[implicit_reducible]

instance MulOpposite.instField {α : Type u_1} [Field α] : Field αᵐᵒᵖ

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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