id — Mathlib · SciLib

English

For any commutative ring R, the identity map R → R is standard-smooth of relative dimension 0.

Русский

Пусть R — коммутативное кольцо. Тождественный гомоморфизм R → R является стандартно гладким относительно размерности 0.

LaTeX

$$$$ \forall R\, [\mathrm{CommRing} R],\; \operatorname{IsStandardSmoothOfRelativeDimension}(0, (\mathrm{RingHom.id} \; R)). $$$$

Lean4

theorem id : IsStandardSmoothOfRelativeDimension 0 (RingHom.id R) :=
  Algebra.IsStandardSmoothOfRelativeDimension.id R

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