English
A variant asserting divisibility of x by the restricted norm image after localization with respect to the integral closure.
Русский
Вариант утверждает делимость x нормированным образом после локализации и ограниченного отображения.
LaTeX
$$$[Algebra.IsSeparable (FractionRing A) (FractionRing B)](x : B) : \\; x \\mid algebraMap A B (intNorm A B x)$$$
Lean4
@[simp]
theorem intNorm_eq_zero {x : B} : Algebra.intNorm A B x = 0 ↔ x = 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⁰
rw [← (IsFractionRing.injective A (FractionRing A)).eq_iff, ← (IsFractionRing.injective B (FractionRing B)).eq_iff]
simp only [algebraMap_intNorm_fractionRing, map_zero, norm_eq_zero_iff]
