Documentation
Atlas
.
AlgebraNotes
.
code
.
NoetherianRings
Search
return to top
source
Imports
Init
Mathlib.RingTheory.Polynomial.Basic
Imported by
NoetherianRings
.
hilbert_basis_theorem
source
theorem
NoetherianRings
.
hilbert_basis_theorem
(
R
:
Type
u_1)
[
CommRing
R
]
[
IsNoetherianRing
R
]
:
IsNoetherianRing
(
Polynomial
R
)