instDivNonZeroDivisors

Mathlib.RingTheory.FractionalIdeal.Operations

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

English

If I,J are fractional with J ≠ 0, I.coeToSubmodule J.coeToSubmodule is fractional.

Русский

Если I,J дробные с J ≠ 0, то I.coeToSubmodule J.coeToSubmodule дробный.

LaTeX

$$IsFractional (nonZeroDivisors R₁) (I.coeToSubmodule J.coeToSubmodule)$$

Lean4

noncomputable instance : Div (FractionalIdeal R₁⁰ K) :=
  ⟨fun I J => if h : J = 0 then 0 else ⟨I / J, fractional_div_of_nonzero h⟩⟩

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

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

Разделы

Аффилиация

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