shrink

Mathlib.RingTheory.Flat.Basic

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

← MathLib Explorer

English

If M is flat, Shrink M is flat (when M is Small).

Русский

Если M плоский модуль, то Shrink M также плоский (если M малый).

LaTeX

$$$Flat\ R\ M \Rightarrow Flat\ R\ (\mathrm{Shrink}\ M)$$$

Lean4

instance shrink [Small.{v'} M] [Flat R M] : Flat R (Shrink.{v'} M) :=
  of_linearEquiv
    (Shrink.linearEquiv R M)
      -- Making this an instance causes an infinite sequence `M → Shrink M → Shrink (Shrink M) → ...`.

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

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

Разделы

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

Аффилиация

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