projective_of_free

Mathlib.Algebra.Category.ModuleCat.Projective

URI: https://scilib.ai/kg/mathlib#ModuleCat.projective_of_free

← MathLib Explorer

English

If a module M has a basis, then M is projective in ModuleCat.

Русский

Если у модуля M есть базис, то он проектируем в ModuleCat.

LaTeX

$$$ (Basis) \Rightarrow (ModuleCat.projective) $$$

Lean4

/-- Modules that have a basis are projective. -/
theorem projective_of_free {ι : Type w} (b : Basis ι R M) : Projective M :=
  have : Module.Projective R M := Module.Projective.of_basis b
  M.projective_of_categoryTheory_projective

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

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

Разделы

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

Аффилиация

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