Documentation

Mathlib.Algebra.Field.Opposite

Field structure on the multiplicative/additive opposite #

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