Documentation
Init
.
Grind
.
CommRing
.
Field
Search
return to top
source
Imports
Init.Grind.CommRing.Basic
Imported by
Lean
.
Grind
.
Field
Lean
.
Grind
.
Field
.
inv_mul_cancel
Lean
.
Grind
.
Field
.
eq_inv_of_mul_eq_one
Lean
.
Grind
.
Field
.
inv_one
Lean
.
Grind
.
Field
.
inv_inv
Lean
.
Grind
.
Field
.
inv_neg
Lean
.
Grind
.
Field
.
inv_eq_zero_iff
Lean
.
Grind
.
Field
.
zero_eq_inv_iff
Lean
.
Grind
.
Field
.
instNoNatZeroDivisorsOfIsCharPOfNatNat
source
class
Lean
.
Grind
.
Field
(
α
:
Type
u)
extends
Lean.Grind.CommRing
α
,
Inv
α
,
Div
α
:
Type
u
add
:
α
→
α
→
α
mul
:
α
→
α
→
α
hPow
:
α
→
Nat
→
α
ofNat
(
n
:
Nat
)
:
OfNat
α
n
natCast
:
NatCast
α
add_assoc
(
a
b
c
:
α
)
:
a
+
b
+
c
=
a
+
(
b
+
c
)
add_comm
(
a
b
:
α
)
:
a
+
b
=
b
+
a
add_zero
(
a
:
α
)
:
a
+
0
=
a
mul_assoc
(
a
b
c
:
α
)
:
a
*
b
*
c
=
a
*
(
b
*
c
)
mul_one
(
a
:
α
)
:
a
*
1
=
a
one_mul
(
a
:
α
)
:
1
*
a
=
a
left_distrib
(
a
b
c
:
α
)
:
a
*
(
b
+
c
)
=
a
*
b
+
a
*
c
right_distrib
(
a
b
c
:
α
)
: (
a
+
b
)
*
c
=
a
*
c
+
b
*
c
zero_mul
(
a
:
α
)
:
0
*
a
=
0
mul_zero
(
a
:
α
)
:
a
*
0
=
0
pow_zero
(
a
:
α
)
:
a
^
0
=
1
pow_succ
(
a
:
α
)
(
n
:
Nat
)
:
a
^
(
n
+
1
)
=
a
^
n
*
a
ofNat_succ
(
a
:
Nat
)
:
OfNat.ofNat
(
a
+
1
)
=
OfNat.ofNat
a
+
1
ofNat_eq_natCast
(
n
:
Nat
)
:
OfNat.ofNat
n
=
↑
n
neg
:
α
→
α
sub
:
α
→
α
→
α
intCast
:
IntCast
α
neg_add_cancel
(
a
:
α
)
:
-
a
+
a
=
0
sub_eq_add_neg
(
a
b
:
α
)
:
a
-
b
=
a
+
-
b
intCast_ofNat
(
n
:
Nat
)
:
↑
(
OfNat.ofNat
n
)
=
OfNat.ofNat
n
intCast_neg
(
i
:
Int
)
:
↑(
-
i
)
=
-
↑
i
mul_comm
(
a
b
:
α
)
:
a
*
b
=
b
*
a
inv
:
α
→
α
div
:
α
→
α
→
α
div_eq_mul_inv
(
a
b
:
α
)
:
a
/
b
=
a
*
b
⁻¹
zero_ne_one :
0
≠
1
inv_zero :
0
⁻¹
=
0
mul_inv_cancel
{
a
:
α
}
:
a
≠
0
→
a
*
a
⁻¹
=
1
Instances
source
theorem
Lean
.
Grind
.
Field
.
inv_mul_cancel
{
α
:
Type
u_1}
[
Field
α
]
{
a
:
α
}
(
h
:
a
≠
0
)
:
a
⁻¹
*
a
=
1
source
theorem
Lean
.
Grind
.
Field
.
eq_inv_of_mul_eq_one
{
α
:
Type
u_1}
[
Field
α
]
{
a
b
:
α
}
(
h
:
a
*
b
=
1
)
:
a
=
b
⁻¹
source
theorem
Lean
.
Grind
.
Field
.
inv_one
{
α
:
Type
u_1}
[
Field
α
]
:
1
⁻¹
=
1
source
theorem
Lean
.
Grind
.
Field
.
inv_inv
{
α
:
Type
u_1}
[
Field
α
]
(
a
:
α
)
:
a
⁻¹
⁻¹
=
a
source
theorem
Lean
.
Grind
.
Field
.
inv_neg
{
α
:
Type
u_1}
[
Field
α
]
(
a
:
α
)
:
(
-
a
)
⁻¹
=
-
a
⁻¹
source
theorem
Lean
.
Grind
.
Field
.
inv_eq_zero_iff
{
α
:
Type
u_1}
[
Field
α
]
{
a
:
α
}
:
a
⁻¹
=
0
↔
a
=
0
source
theorem
Lean
.
Grind
.
Field
.
zero_eq_inv_iff
{
α
:
Type
u_1}
[
Field
α
]
{
a
:
α
}
:
0
=
a
⁻¹
↔
0
=
a
source
instance
Lean
.
Grind
.
Field
.
instNoNatZeroDivisorsOfIsCharPOfNatNat
{
α
:
Type
u_1}
[
Field
α
]
[
IsCharP
α
0
]
:
NoNatZeroDivisors
α