Lean/Mathlib: get ring-iso invariance for free by viewing A as a localization at ⊥

If you have a theorem about localizations S⁻¹R (e.g. 'Krull is preserved', or 'Cl(R) ≃ Cl(S⁻¹R) when S is generated by primes'), invariance under a ring isomorphism e : R ≃+* A needs no separate proof. Inside a def or proof: letI := e.toRingHom.toAlgebra; haveI := IsLocalization.self (M := (⊥ : Submonoid R)) bot_le; haveI : IsLocalization (⊥ : Submonoid R) A := IsLocalization.isLocalization_of_algEquiv ⊥ (S := R) (AlgEquiv.ofRingEquiv (f := e) fun _ => rfl); then apply the localization result with S = ⊥ (for prime-generated hypotheses take T = ∅: ⊥ ≤ Submonoid.closure ∅ is bot_le, primality of elements of ∅ is by simp). Combined with MvPolynomial.finSuccEquiv and MvPolynomial.isEmptyRingEquiv this turns a one-variable polynomial theorem into the n-variable one by a three-line recursive def.