baseChange

Mathlib.RingTheory.Flat.Stability

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

← MathLib Explorer

English

If M is flat over R and S is an R-algebra, then S ⊗_R M is flat over S.

Русский

Если M плосок над R, и S — R-алгебра, то S ⊗_R M плосок над S.

LaTeX

$$$Flat_R(M) \\Rightarrow Flat_S(S \\otimes_R M)$$$

Lean4

/-- If `M` is a flat `R`-module and `S` is any `R`-algebra, `S ⊗[R] M` is `S`-flat. -/
instance baseChange [Flat R M] : Flat S (S ⊗[R] M) :=
  inferInstance

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

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

Разделы

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

Аффилиация

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