algebra

Mathlib.Algebra.Algebra.Basic

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

Lean4

instance _root_.ULift.algebra : Algebra R (ULift A) :=
  {
    ULift.module' with
    algebraMap :=
      { (ULift.ringEquiv : ULift A ≃+* A).symm.toRingHom.comp (algebraMap R A) with
        toFun := fun r => ULift.up (algebraMap R A r) }
    commutes' := fun r x => ULift.down_injective <| Algebra.commutes r x.down
    smul_def' := fun r x => ULift.down_injective <| Algebra.smul_def' r x.down }

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

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

Разделы

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

Аффилиация

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