absNorm_dvd_norm_of_mem

Mathlib.RingTheory.Ideal.Norm.AbsNorm

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

← MathLib Explorer

English

If x ∈ I then absNorm(I) divides normℤ(x).

Русский

Если x ∈ I, то absNorm(I) делит норму ℤ от x.

LaTeX

$$absNorm(I) ∣ normℤ(x) whenever x ∈ I$$

Lean4

theorem absNorm_dvd_norm_of_mem {I : Ideal S} {x : S} (h : x ∈ I) : ↑(Ideal.absNorm I) ∣ Algebra.norm ℤ x :=
  by
  rw [← Int.dvd_natAbs, ← absNorm_span_singleton x, Int.natCast_dvd_natCast]
  exact absNorm_dvd_absNorm_of_le ((span_singleton_le_iff_mem _).mpr h)

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

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

Разделы

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

Аффилиация

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