addMonoidHom_id — Mathlib

English

The mapDomain homomorphism with the identity is the identity homomorphism on finsupps.

Русский

Гомоморфизм mapDomain с тождественным отображением является тождественным гомоморфизмом на Finsupp.

LaTeX

$$$\\text{mapDomain.addMonoidHom }\\mathrm{id} = \\mathrm{AddMonoidHom.id} (\\alpha \\to_{0} M).$$$

Lean4

@[simp]
theorem addMonoidHom_id : mapDomain.addMonoidHom id = AddMonoidHom.id (α →₀ M) :=
  AddMonoidHom.ext fun _ => mapDomain_id

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