addMonoidHom_id — Mathlib

English

mapRange.addMonoidHom with identity maps equals the identity homomorphism.

Русский

mapRange.addMonoidHom с тождественным отображением эквивалентен тождественному гомоморфизму.

LaTeX

$$$\\mathrm{mapRange.addMonoidHom}\\, (\\lambda i, \\mathrm{id}_{\\beta_2 i}) = \\mathrm{id}_{\\Pi_0 i, \\beta_2 i}$$$

Lean4

@[simp]
theorem addMonoidHom_id : (mapRange.addMonoidHom fun i => AddMonoidHom.id (β₂ i)) = AddMonoidHom.id _ :=
  AddMonoidHom.ext mapRange_id

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