map_id — Mathlib

English

The map built from identity on each component equals the identity on the direct sum.

Русский

Гомоморфизм DirectSum, построенный из тождественных отображений на компонентами, равен тождественному отображению на прямой сумме.

LaTeX

$$$$\\mathrm{DirectSum.map}\\, (\\lambda i. \\mathrm{id}_{A_i}) = \\mathrm{id}_{\\bigoplus_i A_i}.$$$$

Lean4

@[simp]
theorem map_id : (map (fun i ↦ AddMonoidHom.id (α i))) = AddMonoidHom.id (⨁ i, α i) :=
  DFinsupp.mapRange.addMonoidHom_id

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