English
Let b be an R-basis of S. The discriminant of the localized basis in R_m equals the localization of the discriminant of b.
Русский
Пусть b — база S как R-модуля. Дискриминант локализованной базы в R_m равен локализации дискриминанта b.
LaTeX
$$$\\operatorname{discr}_{R_m}(\\mathrm{Module.Basis.localizationLocalization\\,R_m\\,M\\,S_m\\, b}) = (\\mathrm{algebraMap}_R^{R_m})(\\operatorname{discr}_R(b)).$$$
Lean4
/-- Let `S` be an extension of `R` and `Rₘ Sₘ` be localizations at `M` of `R S` respectively. Let
`b` be a `R`-basis of `S`. Then discriminant of the `Rₘ`-basis of `Sₘ` induced by `b` is the
discriminant of `b`.
-/
theorem discr_localizationLocalization (b : Basis ι R S) :
Algebra.discr Rₘ (b.localizationLocalization Rₘ M Sₘ) = algebraMap R Rₘ (Algebra.discr R b) := by
rw [Algebra.discr_def, Algebra.discr_def, RingHom.map_det, Algebra.traceMatrix_localizationLocalization]
