Commit 2022-08-24 09:35 94f13c65

feat(ring_theory/localization/away): finitely presented as R[X]/(rX-1) (#12455)

Show localization.away r is isomorphic to R[X]/(rX-1) (implemented as adjoin_root (C r * X - 1)) as R-algebras: localization.away_equiv_adjoin. Lemmas introduced for this purpose are: alg_hom_ext, root_is_inv and alg_hom_subsingleton under namespace adjoin_root, ideal.quotient.alg_hom_ext, is_localization.away.mul_inv_self, and is_localization.alg_hom_subsingleton (which says any two R-alg_hom from from a localization of R to another R-algebra are equal).
Deduce that the R-algebra S is finitely presented if S is a localization of R away from some r : R: is_localization.away.finite_presentation. Lemmas introduced for this purpose are algebra.finite_presentation.polynomial and adjoin_root.finite_presentation, and the finite_type versions are also added.
Golf algebra.finite_finite_type/presentation.mv_polynomial and fix typo in mem_adjoint_support.