coeIdeal_eq_zero'

Mathlib.RingTheory.FractionalIdeal.Basic

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.coeIdeal_eq_zero'

English

The equality (I : FractionalIdeal) = 0 is equivalent to I = ⊥.

Русский

Равенство (I : FractionalIdeal) = 0 эквивалентно I = ⊥.

LaTeX

$$coeIdeal_eq_zero' (h) : (I : FractionalIdeal S P) = 0 ↔ I = (⊥ : Ideal R)$$

Lean4

theorem coeIdeal_eq_zero' {I : Ideal R} (h : S ≤ nonZeroDivisors R) :
    (I : FractionalIdeal S P) = 0 ↔ I = (⊥ : Ideal R) :=
  coeIdeal_inj' h

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

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

Разделы

Аффилиация

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