id — Mathlib · SciLib

English

The canonical presentation of R over itself has no generators and no relations.

Русский

Каноническая презентация кольца R над самим R имеет ноль генераторов и ноль отношений.

LaTeX

$$$\\mathrm{id}\\;:\\; \\mathrm{Presentation}\; R\\; R\\; \\mathrm{PEmpty}\\; \\mathrm{PEmpty}$$$

Lean4

/-- The canonical `R`-presentation of `R` with no generators and no relations. -/
noncomputable def id : Presentation R R PEmpty.{w + 1} PEmpty.{t + 1} :=
  ofBijectiveAlgebraMap Function.bijective_id

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