mathlib3

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

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`.