ulift

Mathlib.LinearAlgebra.FreeModule.Basic

URI: https://scilib.ai/kg/mathlib#Module.Free.ulift

English

If M is free, then ULift M is free.

Русский

Если M свободен, то ULift M свободен.

LaTeX

$$$$ \text{If } M \text{ is free, then } \mathrm{Free}_R(\mathrm{ULift} M) $$$$

Lean4

instance ulift [Free R M] : Free R (ULift M) :=
  of_equiv ULift.moduleEquiv.symm

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

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

Разделы

Аффилиация

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