Field structure on the multiplicative/additive opposite #
Equations
- AddOpposite.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => AddOpposite.op ↑q }
Equations
- MulOpposite.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => MulOpposite.op ↑q }
Equations
- AddOpposite.instRatCast = { ratCast := fun (q : ℚ) => AddOpposite.op ↑q }
Equations
- MulOpposite.instRatCast = { ratCast := fun (q : ℚ) => MulOpposite.op ↑q }
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Equations
- MulOpposite.instDivisionSemiring = DivisionSemiring.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (q : ℚ≥0) => HMul.hMul ↑q) ⋯
Equations
- MulOpposite.instDivisionRing = DivisionRing.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯ ⋯ (fun (q : ℚ) => HMul.hMul ↑q) ⋯
Equations
- MulOpposite.instSemifield = Semifield.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯
Equations
- AddOpposite.instDivisionSemiring = DivisionSemiring.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (q : ℚ≥0) => HMul.hMul ↑q) ⋯
Equations
- AddOpposite.instDivisionRing = DivisionRing.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯ ⋯ (fun (q : ℚ) => HMul.hMul ↑q) ⋯
Equations
- AddOpposite.instSemifield = Semifield.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯