Documentation

Mathlib.Algebra.Field.Opposite

Field structure on the multiplicative/additive opposite #

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.instFieldMulOpposite (α : Type u_1) [inst : 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.instFieldAddOpposite {α : Type u_1} [inst : Field α] :
Equations
  • One or more equations did not get rendered due to their size.