toMonoidHomEquiv_add — Mathlib

English

The correspondence between additive characters and monoid homomorphisms to M preserves addition: toMonoidHomEquiv(ψ+φ) = toMonoidHomEquiv(ψ) · toMonoidHomEquiv(φ).

Русский

Соответствие между аддитивными характеристиками и моноидными гомоморфизмами в M сохраняет сложение: toMonoidHomEquiv(ψ+φ) = toMonoidHomEquiv(ψ)·toMonoidHomEquiv(φ).

LaTeX

$$$\mathrm{toMonoidHomEquiv}(\psi+\phi) = \mathrm{toMonoidHomEquiv}(\psi) \cdot \mathrm{toMonoidHomEquiv}(\phi).$$$

Lean4

@[simp]
theorem toMonoidHomEquiv_add (ψ φ : AddChar A M) : toMonoidHomEquiv (ψ + φ) = toMonoidHomEquiv ψ * toMonoidHomEquiv φ :=
  rfl

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