Documentation

Mathlib.Algebra.Field.Opposite

Field structure on the multiplicative/additive opposite #

source
ink
instance MulOpposite.instDivisionSemiringMulOpposite (α : Type u_1) [inst : DivisionSemiring α] :
DivisionSemiring αᵐᵒᵖ
Equations
  • One or more equations did not get rendered due to their size.
source
ink
instance MulOpposite.instDivisionRingMulOpposite (α : Type u_1) [inst : DivisionRing α] :
DivisionRing αᵐᵒᵖ
Equations
  • One or more equations did not get rendered due to their size.
source
ink
instance MulOpposite.instSemifieldMulOpposite (α : Type u_1) [inst : Semifield α] :
Semifield αᵐᵒᵖ
Equations
  • One or more equations did not get rendered due to their size.
source
ink
instance MulOpposite.instFieldMulOpposite (α : Type u_1) [inst : Field α] :
Field αᵐᵒᵖ
Equations
  • One or more equations did not get rendered due to their size.
source
ink
instance AddOpposite.instDivisionSemiringAddOpposite {α : Type u_1} [inst : DivisionSemiring α] :
DivisionSemiring αᵃᵒᵖ
Equations
  • One or more equations did not get rendered due to their size.
source
ink
instance AddOpposite.instDivisionRingAddOpposite {α : Type u_1} [inst : DivisionRing α] :
DivisionRing αᵃᵒᵖ
Equations
  • One or more equations did not get rendered due to their size.
source
ink
instance AddOpposite.instSemifieldAddOpposite {α : Type u_1} [inst : Semifield α] :
Semifield αᵃᵒᵖ
Equations
  • One or more equations did not get rendered due to their size.
source
ink
instance AddOpposite.instFieldAddOpposite {α : Type u_1} [inst : Field α] :
Field αᵃᵒᵖ
Equations
  • One or more equations did not get rendered due to their size.