relNorm_relNorm — Mathlib

English

For I ⊆ R, relNorm_R(I.map(algebraMap_R_S)) equals I raised to the finrank of FractionR to FractionS.

Русский

Для идеала I ⊆ R выполняется relNorm_R(I.map(algebraMap_R_S)) = I^{finrank(FractionRing R, FractionRing S)}.

LaTeX

$$$\mathrm{relNorm}_R(I) = I^{\mathrm{finrank}(\mathrm{FractionRing}(R), \mathrm{FractionRing}(S))}$$$

Lean4

theorem relNorm_relNorm (T : Type*) [CommRing T] [IsDedekindDomain T] [IsIntegrallyClosed T] [Algebra R T] [Algebra T S]
    [IsScalarTower R T S] [Module.Finite R T] [Module.Finite T S] [NoZeroSMulDivisors R T] [NoZeroSMulDivisors T S]
    (I : Ideal S) : relNorm R (relNorm T I) = relNorm R I :=
  spanNorm_spanNorm _ _ _

Похожие утверждения