divisionSemiring

Mathlib.Algebra.Field.ULift

URI: https://scilib.ai/kg/mathlib#ULift.divisionSemiring

Lean4

instance divisionSemiring [DivisionSemiring α] : DivisionSemiring (ULift α)
    where
  nnqsmul q x := up (DivisionSemiring.nnqsmul q x.down)
  nnqsmul_def _ _ := congrArg up <| DivisionSemiring.nnqsmul_def _ _
  nnratCast_def _ := congrArg up <| DivisionSemiring.nnratCast_def _

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

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

Разделы

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

Аффилиация

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