mathlib3 documentation

algebra.field.opposite

Field structure on the multiplicative/additive opposite #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem add_opposite.op_rat_cast {α : Type u_1} [has_rat_cast α] (q : ) :
@[simp, norm_cast]
theorem mul_opposite.op_rat_cast {α : Type u_1} [has_rat_cast α] (q : ) :
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.field (α : Type u_1) [field α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def add_opposite.field (α : Type u_1) [field α] :
Equations