relNorm_le_comap — Mathlib

English

Given towers R ⊆ T ⊆ S of Dedekind domains with finite modules, relNorm_R(relNorm_T(I)) = relNorm_R(I).

Русский

Пусть R ⊆ T ⊆ S — цепочка Дедекендовых доменов с конечными модулями; тогда relNorm_R(relNorm_T(I)) = relNorm_R(I).

LaTeX

$$$\\mathrm{relNorm}_R( \\mathrm{relNorm}_T(I) ) = \\mathrm{relNorm}_R(I)$$$

Lean4

theorem relNorm_le_comap [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (I : Ideal S) :
    relNorm R I ≤ comap (algebraMap R S) I :=
  spanNorm_le_comap R I

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