mathlib

96c80e24 - feat(ring_theory/localization): Localizations of integral extensions (#3942)

feat(ring_theory/localization): Localizations of integral extensions (#3942) The main definition is the algebra induced by localization at an algebra. Given an algebra `R → S` and a submonoid `M` of `R`, as well as localization maps `f : R → Rₘ` and `g : S → Sₘ`, there is a natural algebra `Rₘ → Sₘ` that makes the entire square commute, and this is defined as `localization_algebra`. The two main theorems are similar but distinct statements about integral elements and localizations: * `is_integral_localization_at_leading_coeff` says that if an element `x` is algebraic over `algebra R S`, then if we localize to a submonoid containing the leading coefficient the image of `x` will be integral. * `is_integral_localization` says that if `R → S` is an integral extension, then the algebra induced by localizing at any particular submonoid will be an integral extension. Co-authored-by: Devon Tuma <dtumad@gmail.com>