Field structure on the multiplicative/additive opposite

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

Equations

• MulOpposite.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => MulOpposite.op ↑q }

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

Equations

• AddOpposite.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => AddOpposite.op ↑q }

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

Equations

• MulOpposite.instRatCast = { ratCast := fun (q : ℚ) => MulOpposite.op ↑q }

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

Equations

• AddOpposite.instRatCast = { ratCast := fun (q : ℚ) => AddOpposite.op ↑q }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• MulOpposite.instDivisionSemiring = DivisionSemiring.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯

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

Equations

• MulOpposite.instDivisionRing = DivisionRing.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯ ⋯ (fun (x : ℚ) => HMul.hMul ↑x) ⋯

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

Equations

• MulOpposite.instSemifield = Semifield.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯

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

Equations

• MulOpposite.instField = Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯ ⋯ DivisionRing.qsmul ⋯

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

Equations

• AddOpposite.instDivisionSemiring = DivisionSemiring.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯

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

Equations

• AddOpposite.instDivisionRing = DivisionRing.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯ ⋯ (fun (x : ℚ) => HMul.hMul ↑x) ⋯

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

Equations

• AddOpposite.instSemifield = Semifield.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯

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

Equations

• AddOpposite.instField = Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯ ⋯ DivisionRing.qsmul ⋯