id — Mathlib · SciLib

English

For any commutative ring R, the identity map id_R : R → R is flat; equivalently, R is a flat module over itself.

Русский

Для любого коммутативного кольца R отображение идентичности id_R: R → R является плоским; эквивалентно тому, что R является плоским модулем над R.

LaTeX

$$$\\forall R \, [\\mathrm{CommRing} \, R],\\ Flat(\\mathrm{id}_R)$$$

Lean4

/-- The identity of a ring is flat. -/
theorem id : RingHom.Flat (RingHom.id R) :=
  Module.Flat.self

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