Documentation

Mathlib.Algebra.Field.Opposite

Field structure on the multiplicative/additive opposite #

Equations
Equations
Equations
Equations
@[simp]
theorem AddOpposite.op_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
AddOpposite.op q = q
@[simp]
theorem MulOpposite.op_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
MulOpposite.op q = q
@[simp]
theorem AddOpposite.unop_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
@[simp]
theorem MulOpposite.unop_nnratCast {α : Type u_1} [NNRatCast α] (q : ℚ≥0) :
@[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 : ) :
@[simp]
theorem MulOpposite.unop_ratCast {α : Type u_1} [RatCast α] (q : ) :
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.
instance MulOpposite.instField {α : Type u_1} [Field α] :
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.
instance AddOpposite.instField {α : Type u_1} [Field α] :
Equations
  • One or more equations did not get rendered due to their size.