Documentation

Mathlib.Algebra.Field.Opposite

Field structure on the multiplicative/additive opposite #

instance AddOpposite.ratCast (α : Type u_1) [RatCast α] :
Equations
instance MulOpposite.ratCast (α : Type u_1) [RatCast α] :
Equations
@[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.field (α : 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.field {α : Type u_1} [Field α] :
Equations