English
In the fraction-ring setting, the algebra map commutes with intNorm on x, equating two equivalent definitions of the norm.
Русский
В настройке дробной оболочки отображение по основанию согласуется с intNorm на x, давая равные определения нормы.
LaTeX
$$$[IsIntegralClosure B A (FractionRing B)]\\[IsLocalization (algebraMapSubmonoid B A^0) (FractionRing B)]\\Rightarrow algebraMap A (FractionRing A) (Algebra.intNorm A B x) = Algebra.norm (FractionRing A) (algebraMap B (FractionRing B) x)$$$
Lean4
@[simp]
theorem intNorm_zero : Algebra.intNorm A B 0 = 0 :=
by
haveI : IsIntegralClosure B A (FractionRing B) := IsIntegralClosure.of_isIntegrallyClosed _ _ _
haveI : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
IsIntegralClosure.isLocalization _ (FractionRing A) _ _
haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
apply IsFractionRing.injective A (FractionRing A)
simp
