absNorm_under_mem

Mathlib.RingTheory.Ideal.Int

URI: https://scilib.ai/kg/mathlib#Int.absNorm_under_mem

English

The element absNorm(under ℤ I) (taken in R) belongs to I.

Русский

Элемент absNorm(under ℤ I), взятый в R, принадлежит I.

LaTeX

$$$(\operatorname{absNorm}(\operatorname{under} \mathbb{Z} I) : R) \in I$$$

Lean4

theorem absNorm_under_mem : (absNorm (under ℤ I) : R) ∈ I := by rw [← cast_natCast, cast_mem_ideal_iff]

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

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

Разделы

Аффилиация

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