homogeneous_localization): homogeneous localization ring is local (#13071)

Commit

3 years ago

feat(ring_theory/graded_algebra/homogeneous_localization): homogeneous localization ring is local (#13071) showed that `local_ring (homogeneous_localization 𝒜 x)` from prime ideal `x`

Author

jjaassoonn

Parents

3e4bf5de

mathlib3 be147af1 - feat(ring_theory/graded_algebra/homogeneous_localization): homogeneous localization ring is local (#13071)

mathlib3
be147af1 - feat(ring_theory/graded_algebra/homogeneous_localization): homogeneous localization ring is local (#13071)