instRootableBy

Mathlib.GroupTheory.Divisible

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

Lean4

@[to_additive]
instance instRootableBy [RootableBy A α] : RootableBy (ULift A) α
    where
  root x a := ULift.up <| RootableBy.root x.down a
  root_zero x := ULift.ext _ _ <| RootableBy.root_zero x.down
  root_cancel _ h := ULift.ext _ _ <| RootableBy.root_cancel _ h

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

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

Разделы

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

Аффилиация

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