norm_mem_relNorm — Mathlib

English

If S is finite and free over R, and x ∈ I with I ⊆ S, then Algebra.norm_R(x) ∈ relNorm_R(I).

Русский

Если S конечна и свободна над R, и x ∈ I, то Norm_R(x) принадлежит relNorm_R(I).

LaTeX

$$$\text{norm}_R(x) \in \mathrm{relNorm}_R(I) \quad\text{whenever } x \in I \subseteq S.$$$

Lean4

theorem norm_mem_relNorm [Module.Free R S] (I : Ideal S) {x : S} (hx : x ∈ I) : Algebra.norm R x ∈ relNorm R I :=
  norm_mem_spanNorm R x hx

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