English
There is a local-homomorphism structure for the natural algebra map between valuationSubrings on the base and extension rings.
Русский
Существует структура локального гомоморфизма для естественного отображения между valuationSubrings базового и расширенного колец.
LaTeX
$$$IsLocalHom\\bigl(\\operatorname{algebraMap}(vK^{\\mathrm{integer}} , vL^{\\mathrm{integer}})\\bigr)$$$
Lean4
instance : Ideal.LiesOver (maximalIdeal L₀) (maximalIdeal K₀) :=
⟨(maximalIdeal_comap_algebraMap_eq_maximalIdeal _ _).symm⟩
