extend_to_localization): Extending valuations to localizations. (#13610)

Commit

3 years ago

feat(ring_theory/valuation/extend_to_localization): Extending valuations to localizations. (#13610) Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

Author

adamtopaz

Parents

fe2917a4

mathlib3 64b3576f - feat(ring_theory/valuation/extend_to_localization): Extending valuations to localizations. (#13610)

mathlib3
64b3576f - feat(ring_theory/valuation/extend_to_localization): Extending valuations to localizations. (#13610)