relNorm_apply — Mathlib

English

For a Dedekind extension, relNorm(I) equals the span of the norms of elements of I: relNorm(I) = span(Algebra.intNorm_R_S '' (I : Set S)).

Русский

При удовлетворяющем условиям расширении дано равенство relNorm(I) = span(Algebra.intNorm_R_S '' (I : Set S)).

LaTeX

$$$\mathrm{relNorm}(I) = \operatorname{span}\big( \mathrm{Algebra.intNorm}_{R,S} \big[ I \big] \big).$$$

Lean4

theorem relNorm_apply (I : Ideal S) : relNorm R I = span (Algebra.intNorm R S '' (I : Set S) : Set R) :=
  rfl

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