instModuleIsReflexive

Mathlib.LinearAlgebra.Dual.Lemmas

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

English

The ULift of a module is IsReflexive over the same ring.

Русский

ULift-модуль над тем же кольцом сохраняет рефлексивность.

LaTeX

$$IsReflexive R (ULift M)$$

Lean4

instance _root_.ULift.instModuleIsReflexive.{w} : IsReflexive R (ULift.{w} M) :=
  equiv ULift.moduleEquiv.symm

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

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

Разделы

Аффилиация

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