English
If S is the localization of R at a submonoid M, then MvPolynomial(σ,S) is the localization of MvPolynomial(σ,R) at the submonoid M.map C.
Русский
Если S — локализация R по подмоноиду M, то MvPolynomial(σ,S) — локализация MvPolynomial(σ,R) по подмоноиду M.map C.
LaTeX
$$IsLocalization (M.map C) (MvPolynomial σ S)$$
Lean4
/-- If `S` is the localization of `R` at a submonoid `M`, then `MvPolynomial σ S`
is the localization of `MvPolynomial σ R` at `M.map MvPolynomial.C`.
See also `Polynomial.isLocalization` for the univariate case. -/
instance isLocalization : IsLocalization (M.map <| C (σ := σ)) (MvPolynomial σ S) :=
isLocalizedModule_iff_isLocalization.mp <|
(isLocalizedModule_iff_isBaseChange M S _).mpr <|
.of_equiv (algebraTensorAlgEquiv _ _).toLinearEquiv fun _ ↦ by simp
