toMonoidHomEquiv_zero — Mathlib

English

Under the canonical isomorphism between AddChar A M and MonoidHom(A, M), the zero element corresponds to the identity hom: toMonoidHomEquiv(0) = 1.

Русский

Согласно каноническому изоморфизму AddChar A M и MonoidHom(A, M), нулевой элемент соответствует тождественному однородному отображению: toMonoidHomEquiv(0) = 1.

LaTeX

$$$$ \mathrm{toMonoidHomEquiv}(0) = 1. $$$$

Lean4

@[simp]
theorem toMonoidHomEquiv_zero : toMonoidHomEquiv (0 : AddChar A M) = 1 :=
  rfl

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