id_apply' — Mathlib

English

The toFun' of the identity polynomial law is the standard identity map on every coefficient ring.

Русский

toFun' тождественного полиномального закона равен стандартному тождественному отображению на каждом кольце-коэффициенте.

LaTeX

$$$\text{ id }^{\mathrm{toFun}'}_S = \mathrm{id}$ for all S.$$

Lean4

theorem id_apply' {S : Type u} [CommSemiring S] [Algebra R S] : (id : M →ₚₗ[R] M).toFun' S = _root_.id :=
  rfl

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