absNorm_mem

Mathlib.RingTheory.Ideal.Norm.AbsNorm

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

← MathLib Explorer

English

The norm of I contains absNorm(I) as an element of I.

Русский

Норма(I) содержит absNorm(I) как элемент I.

LaTeX

$$absNorm(I) ∈ I$$

Lean4

theorem absNorm_mem (I : Ideal S) : ↑(Ideal.absNorm I) ∈ I := by
  rw [absNorm_apply, cardQuot, ← Ideal.Quotient.eq_zero_iff_mem, map_natCast, Quotient.index_eq_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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