instInvOneClassNonZeroDivisors

Mathlib.RingTheory.FractionalIdeal.Inverse

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

English

There is a canonical InvOneClass structure on FractionalIdeal (nonZeroDivisors R) K, with inv_one defined as div_one.

Русский

Существует каноническая структура обратимости на FractionalIdeal (nonZeroDivisors R) K, где inv_one определяется как div_one.

LaTeX

$$inv(1) = 1$$

Lean4

noncomputable instance : InvOneClass (FractionalIdeal R₁⁰ K) :=
  { inv_one := div_one }

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

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

Разделы

Аффилиация

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