instDivisionRing

Mathlib.Algebra.Field.Opposite

URI: https://scilib.ai/kg/mathlib#AddOpposite.instDivisionRing

Lean4

instance instDivisionRing [DivisionRing α] : DivisionRing αᵃᵒᵖ
    where
  __ := instRing
  __ := instDivisionSemiring
  qsmul := _
  qsmul_def := fun _ _ => rfl
  ratCast_def
    q := unop_injective <| by rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast, unop_intCast, div_eq_mul_inv]

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

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

Разделы

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

Аффилиация

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