le_div_iff_of_nonzero

Mathlib.RingTheory.FractionalIdeal.Operations

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

← MathLib Explorer

English

If I ≤ 1, then I ≤ I * (1 / I).

Русский

Если I ≤ 1, то I ≤ I * (1 / I).

LaTeX

$$I ≤ 1 → I ≤ I * (1 / I)$$

Lean4

theorem le_div_iff_of_nonzero {I J J' : FractionalIdeal R₁⁰ K} (hJ' : J' ≠ 0) :
    I ≤ J / J' ↔ ∀ x ∈ I, ∀ y ∈ J', x * y ∈ J :=
  ⟨fun h _ hx => (mem_div_iff_of_nonzero hJ').mp (h hx), fun h x hx => (mem_div_iff_of_nonzero hJ').mpr (h x hx)⟩

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

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

Разделы

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

Аффилиация

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