instInvNonZeroDivisors

Mathlib.RingTheory.FractionalIdeal.Inverse

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

English

For any fractional ideal I, its inverse coincides with the reciprocal, i.e., I^{-1} = 1 / I.

Русский

Для любого дробного идеала I обратный к нему совпадает с его обратной величиной, то есть I^{-1} = 1 / I.

LaTeX

$$$$I^{-1} = \dfrac{1}{I}.$$$$

Lean4

noncomputable instance : Inv (FractionalIdeal R₁⁰ K) :=
  ⟨fun I => 1 / I⟩

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

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

Разделы

Аффилиация

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