inv'

Mathlib.RingTheory.OreLocalization.NonZeroDivisors

URI: https://scilib.ai/kg/mathlib#OreLocalization.inv'

Lean4

noncomputable instance inv' : Inv R[R⁰⁻¹] :=
  ⟨OreLocalization.inv⟩

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

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

Разделы

Аффилиация

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