prod_normalizedFactors_eq_self

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

URI: https://scilib.ai/kg/mathlib#prod_normalizedFactors_eq_self

English

For a nonzero ideal I in a Dedekind domain, the product of its normalized factors equals I.

Русский

Для не нулевого идеала I в области Дедекина произведение его нормализованных факторов равно I.

LaTeX

$$(normalizedFactors I).prod = I$$

Lean4

theorem prod_normalizedFactors_eq_self (hI : I ≠ ⊥) : (normalizedFactors I).prod = I :=
  associated_iff_eq.1 (prod_normalizedFactors hI)

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

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

Разделы

Аффилиация

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