of_projective

Mathlib.RingTheory.Flat.Basic

URI: https://scilib.ai/kg/mathlib#Module.Flat.of_projective

English

A projective module is flat.

Русский

Проективный модуль плосок.

LaTeX

$$$Flat\ R\ M$ if $M$ is projective.$$

Lean4

instance of_projective [Projective R M] : Flat R M :=
  have ⟨e, he⟩ := Module.projective_def'.mp ‹_›
  of_retract _ _ he

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

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

Разделы

Аффилиация

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