isNoetherian_zero

Mathlib.RingTheory.FractionalIdeal.Operations

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.isNoetherian_zero

← MathLib Explorer

English

The numerator of a fractional ideal is contained in the ideal itself.

Русский

Числитель дробного идеала содержится в самом идеале.

LaTeX

$$(I.num : FractionalIdeal S P) ≤ I$$

Lean4

theorem isNoetherian_zero : IsNoetherian R₁ (0 : FractionalIdeal R₁⁰ K) :=
  isNoetherian_submodule.mpr fun I (hI : I ≤ (0 : FractionalIdeal R₁⁰ K)) =>
    by
    rw [coe_zero, le_bot_iff] at hI
    rw [hI]
    exact fg_bot

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

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

Разделы

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

Аффилиация

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