id_apply — Mathlib

English

For any commutative ring R and element r ∈ R, the identity morphism acts as the identity: (id_R)(r) = r.

Русский

Для любого коммутативного кольца R и элемента r ∈ R тождественный морфизм действует как тождественный отображение: (id_R)(r) = r.

LaTeX

$$$ (\mathrm{id}_R)(r) = r \quad \text{for all } r \in R.$$$

Lean4

theorem id_apply (R : CommRingCat) (r : R) : (𝟙 R : R ⟶ R) r = r := by simp

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