Documentation
Mathlib
.
RingTheory
.
KrullDimension
.
Field
Search
return to top
source
Imports
Init
Mathlib.RingTheory.KrullDimension.Basic
Imported by
ringKrullDim_eq_zero_of_field
ringKrullDim_eq_zero_of_isField
The Krull dimension of a field
#
This file proves that the Krull dimension of a field is zero.
source
@[simp]
theorem
ringKrullDim_eq_zero_of_field
(F :
Type
u_1)
[
Field
F
]
:
ringKrullDim
F
=
0
source
theorem
ringKrullDim_eq_zero_of_isField
{F :
Type
u_1}
[
CommRing
F
]
(hF :
IsField
F
)
:
ringKrullDim
F
=
0