instDivisionSemiring

Mathlib.Algebra.Field.Opposite

URI: https://scilib.ai/kg/mathlib#MulOpposite.instDivisionSemiring

Lean4

instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵐᵒᵖ
    where
  __ := instSemiring
  __ := instGroupWithZero
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  nnratCast_def
    q :=
    unop_injective <| by
      rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast, NNRat.cast_def, div_eq_mul_inv, Nat.cast_comm]

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

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

Разделы

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

Аффилиация

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