div_nonzero

Mathlib.RingTheory.FractionalIdeal.Operations

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

English

If J ≠ 0, then I / J is a well-defined fractional ideal.

Русский

Если J ≠ 0, тогда I / J определено как дробный идеал.

LaTeX

$$div_nonzero$$

Lean4

theorem div_nonzero {I J : FractionalIdeal R₁⁰ K} (h : J ≠ 0) : I / J = ⟨I / J, fractional_div_of_nonzero h⟩ :=
  dif_neg h

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

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

Разделы

Аффилиация

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