dfinsupp

Mathlib.RingTheory.Flat.Basic

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

English

If every Mi is flat, then the DFinsupp is flat.

Русский

Если каждый Mi плосок, то DFinsupp плосок.

LaTeX

$$$Flat\ R\ (DFinsupp fun i => M_i) \Rightarrow \forall i, Flat\ R\ (M_i)$$$

Lean4

instance dfinsupp [∀ i, Flat R (M i)] : Flat R (Π₀ i, M i) :=
  dfinsupp_iff.mpr ‹_›

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

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

Разделы

Аффилиация

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