id'_coe — Mathlib

English

The underlying function of id' equals the ordinary identity function when σ is the identity.

Русский

Базовая функция id' равна обычной функции идентичности, когда σ — тождественный гомоморфизм.

LaTeX

$$$\big(\mathrm{id'} : M \to_\sigma M\big)\!:\ M \to M = \mathrm{id}$$$

Lean4

@[simp, norm_cast]
theorem id'_coe {σ : R →+* R} [RingHomId σ] : ((id' : M →ₛₗ[σ] M) : M → M) = _root_.id :=
  rfl

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