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
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.