compAddChar — Mathlib

English

Composing a monoid hom with an additive character yields another additive character, given by composition with the original map.

Русский

Композиция моноид-гомоморфизма с аддитивным характером дает новый характер, реализованный через композицию исходных отображений.

LaTeX

$$$$ \text{compAddChar}(f, \phi) = \text{the additive character } a \mapsto f(\phi(a)). $$$$

Lean4

/-- Composing a `MonoidHom` with an `AddChar` yields another `AddChar`. -/
def _root_.MonoidHom.compAddChar {N : Type*} [Monoid N] (f : M →* N) (φ : AddChar A M) : AddChar A N :=
  toMonoidHomEquiv.symm (f.comp φ.toMonoidHom)

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