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