map_id — Mathlib

English

Let R be a semiring. The map on power series induced by the identity ring homomorphism is the identity on the power series ring R⟦X⟧.

Русский

Пусть R — полукольцо. Отображение степенных рядов, получаемое от тождественного кольцевого гомоморфа, является тождественным отображением на кольце степенных рядов R⟦X⟧.

LaTeX

$$$\mathrm{PowerSeries.map}(\mathrm{RingHom.id}\,R) = \mathrm{id}_{R⟦X⟧}$$$

Lean4

@[simp]
theorem map_id : (map (RingHom.id R) : R⟦X⟧ → R⟦X⟧) = id :=
  rfl

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