mathlib documentation

algebra.field.opposite

Field structure on the multiplicative/additive opposite #

@[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