instSemifield

Mathlib.Algebra.Field.Rat

URI: https://scilib.ai/kg/mathlib#NNRat.instSemifield

Lean4

instance instSemifield : Semifield ℚ≥0 where
  inv_zero := by ext; simp
  mul_inv_cancel q h := by ext; simp [h]
  nnratCast_def q := q.num_div_den.symm
  nnqsmul q a := q * a
  nnqsmul_def q a := rfl
  zpow n a := a ^ n
  zpow_zero' a := by ext; apply Field.zpow_zero'
  zpow_succ' n a := by ext; apply Field.zpow_succ'
  zpow_neg' n a := by ext; apply Field.zpow_neg'

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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