relNorm_mono

Mathlib.RingTheory.Ideal.Norm.RelNorm

URI: https://scilib.ai/kg/mathlib#Ideal.relNorm_mono

English

For an algebra equivalence σ: S ≃ₐ[R] T, relNorm_R(I.map σ) = relNorm_R(I).

Русский

Для алгебраического эквивалента σ: S ≃ₐ[R] T выполняется relNorm_R(I.map σ) = relNorm_R(I).

LaTeX

$$$\mathrm{relNorm}_R( I \mapsto \sigma ) = \mathrm{relNorm}_R(I)$$$

Lean4

@[mono]
theorem relNorm_mono {I J : Ideal S} (h : I ≤ J) : relNorm R I ≤ relNorm R J :=
  spanNorm_mono R h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru