Documentation
Mathlib
.
Algebra
.
Field
.
Opposite
Search
Google site search
Mathlib
.
Algebra
.
Field
.
Opposite
source
Imports
Init
Mathlib.Algebra.Field.Defs
Mathlib.Algebra.Ring.Opposite
Mathlib.Data.Int.Cast.Lemmas
Imported by
AddOpposite
.
ratCast
MulOpposite
.
ratCast
AddOpposite
.
op_ratCast
MulOpposite
.
op_ratCast
AddOpposite
.
unop_ratCast
MulOpposite
.
unop_ratCast
MulOpposite
.
divisionSemiring
MulOpposite
.
divisionRing
MulOpposite
.
semifield
MulOpposite
.
field
AddOpposite
.
divisionSemiring
AddOpposite
.
divisionRing
AddOpposite
.
semifield
AddOpposite
.
field
Field structure on the multiplicative/additive opposite
#
source
instance
AddOpposite
.
ratCast
(α :
Type
u_1)
[
RatCast
α
]
:
RatCast
α
ᵃᵒᵖ
source
instance
MulOpposite
.
ratCast
(α :
Type
u_1)
[
RatCast
α
]
:
RatCast
α
ᵐᵒᵖ
source
@[simp]
theorem
AddOpposite
.
op_ratCast
{α :
Type
u_1}
[
RatCast
α
]
(q :
ℚ
)
:
AddOpposite.op
↑
q
=
↑
q
source
@[simp]
theorem
MulOpposite
.
op_ratCast
{α :
Type
u_1}
[
RatCast
α
]
(q :
ℚ
)
:
MulOpposite.op
↑
q
=
↑
q
source
@[simp]
theorem
AddOpposite
.
unop_ratCast
{α :
Type
u_1}
[
RatCast
α
]
(q :
ℚ
)
:
AddOpposite.unop
↑
q
=
↑
q
source
@[simp]
theorem
MulOpposite
.
unop_ratCast
{α :
Type
u_1}
[
RatCast
α
]
(q :
ℚ
)
:
MulOpposite.unop
↑
q
=
↑
q
source
instance
MulOpposite
.
divisionSemiring
(α :
Type
u_1)
[
DivisionSemiring
α
]
:
DivisionSemiring
α
ᵐᵒᵖ
source
instance
MulOpposite
.
divisionRing
(α :
Type
u_1)
[
DivisionRing
α
]
:
DivisionRing
α
ᵐᵒᵖ
source
instance
MulOpposite
.
semifield
(α :
Type
u_1)
[
Semifield
α
]
:
Semifield
α
ᵐᵒᵖ
source
instance
MulOpposite
.
field
(α :
Type
u_1)
[
Field
α
]
:
Field
α
ᵐᵒᵖ
source
instance
AddOpposite
.
divisionSemiring
{α :
Type
u_1}
[
DivisionSemiring
α
]
:
DivisionSemiring
α
ᵃᵒᵖ
source
instance
AddOpposite
.
divisionRing
{α :
Type
u_1}
[
DivisionRing
α
]
:
DivisionRing
α
ᵃᵒᵖ
source
instance
AddOpposite
.
semifield
{α :
Type
u_1}
[
Semifield
α
]
:
Semifield
α
ᵃᵒᵖ
source
instance
AddOpposite
.
field
{α :
Type
u_1}
[
Field
α
]
:
Field
α
ᵃᵒᵖ