Revision #1854 → #2537 · back to history
modifiedRing of continuous functions79df1e0c3bb4
| Field | From #1854 | To #2537 |
|---|
| mathlib.decl | ContinuousMap.instCommRing | ContinuousMap.instCommRingOfIsTopologicalRing |
| provenance | ai | ai-moderated |
modifiedNoetherian local rings have finite dimensionb0417f77d965
| Field | From #1854 | To #2537 |
|---|
| mathlib.decl | AlgebraicGeometry.instFiniteRingKrullDim | instFiniteRingKrullDimOfIsLocalRing |
| provenance | ai | ai-moderated |
modifiedDimension inequality for Noetherian local ringsff1c3d5b9408
| Field | From #1854 | To #2537 |
|---|
| mathlib.decl | IsLocalRing.ringKrullDim_le_spanFinrank_maximalIdeal | ringKrullDim_le_spanFinrank_maximalIdeal |
| provenance | ai | ai-moderated |