coe_one — Mathlib

English

The identity endomorphism corresponds to the identity function when viewed as a function: the underlying function of 1 is id.

Русский

Идентичный эндоморфизм, рассматриваемый как функция, соответствует тождественной функции: база 1 превращается в id.

LaTeX

$$$ \uparrow 1 = \mathrm{id} $ (as functions)$$

Lean4

theorem coe_one : ⇑(1 : Module.End R M) = _root_.id :=
  rfl

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