self

Mathlib.RingTheory.Flat.Basic

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

← MathLib Explorer

English

The ring R, considered as a module over itself, is flat.

Русский

Кольцо R, рассматриваемое как модуль над самим собой, плоское.

LaTeX

$$Flat R R$$

Lean4

instance self : Flat R R where
  out _ _ _ _ I
    _ := by
    rw [← (TensorProduct.rid R I).symm.injective_comp, ← (TensorProduct.rid R _).comp_injective]
    convert Subtype.coe_injective using 1
    ext; simp

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

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

Разделы

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

Аффилиация

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