instDivInvOneMonoid

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.instDivInvOneMonoid

Lean4

noncomputable instance : DivInvOneMonoid EReal where
  inv_one := by nth_rw 1 [← coe_one, ← coe_inv 1, _root_.inv_one, coe_one]

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

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

Разделы

Аффилиация

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