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
Equations
  • One or more equations did not get rendered due to their size.
Equations
instance MulOpposite.instField (α : Type u_1) [Field α] :
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
instance AddOpposite.instField {α : Type u_1} [Field α] :
Equations
  • AddOpposite.instField = let __src := AddOpposite.instDivisionRing; let __src_1 := AddOpposite.instCommRing α; Field.mk DivisionRing.zpow DivisionRing.qsmul