spanNorm — Mathlib

English

Let R ⊆ S and T be rings with appropriate integrality; for any ideal I of S, spanNorm R I is below spanNorm R (spanNorm T I).

Русский

Пусть R, S, T — кольца с надлежащими свойствами; для любого идеала I в S выполняется spanNorm_R(I) ≤ spanNorm_R(spanNorm_T(I)).

LaTeX

$$$$\forall I:\mathrm{Ideal}(S),\; \operatorname{spanNorm}(R,I) \le \operatorname{spanNorm}(R,\operatorname{spanNorm}(T,I)).$$$$

Lean4

/-- `Ideal.spanNorm R (I : Ideal S)` is the ideal generated by mapping `Algebra.intNorm R S`
over `I`.

See also `Ideal.relNorm`.
-/
noncomputable def spanNorm (I : Ideal S) : Ideal R :=
  Ideal.map (Algebra.intNorm R S) I

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