flat

Mathlib.RingTheory.RingHom.FaithfullyFlat

URI: https://scilib.ai/kg/mathlib#RingHom.FaithfullyFlat.flat

English

FaithfullyFlat implies flatness.

Русский

FaithfullyFlat implies flatness.

LaTeX

$$$f\\text{ FaithfullyFlat} \\Rightarrow f.\\text{Flat}$$$

Lean4

theorem flat (hf : f.FaithfullyFlat) : f.Flat := by
  algebraize [f]
  exact inferInstanceAs <| Module.Flat R S

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

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

Разделы

Аффилиация

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