toAddMonoidHomEquiv_symm_zero — Mathlib

English

The inverse of the AddMonoidHom equivalence sends 0 to the zero additive character: toAddMonoidHomEquiv.symm(0) = 0.

Русский

Обратное отображение эквивалентности AddMonoidHom отправляет 0 в нулевой аддитивный характер: toAddMonoidHomEquiv.symm(0) = 0.

LaTeX

$$$$ \mathrm{toAddMonoidHomEquiv}.\mathrm{symm}(0) = 0. $$$$

Lean4

@[simp]
theorem toAddMonoidHomEquiv_symm_zero : toAddMonoidHomEquiv.symm (0 : A →+ Additive M) = 0 :=
  rfl

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