map_one — Mathlib

English

The map sends the unit Hahn series to the unit Hahn series after applying a monoid-with-zero homomorphism, i.e., it preserves 1.

Русский

Карта сохраняет единицу: отображение единицы ГансСерии через гомоморфизм моноида сохраняет единицу.

LaTeX

$$$\mathrm{HahnSeries}.map 1 = 1$$$

Lean4

@[simp]
protected theorem map_one [MonoidWithZero R] [MonoidWithZero S] (f : R →*₀ S) :
    (1 : HahnSeries Γ R).map f = (1 : HahnSeries Γ S) :=
  HahnSeries.map_single (a := (0 : Γ)) f.toZeroHom |>.trans <| congrArg _ <| f.map_one

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