charMonoidHom — Mathlib

English

For any w ∈ Multiplicative W and v ∈ V, the evaluation of charMonoidHom at w and then at v gives e(L(v,w)).

Русский

Для любого w ∈ W и v ∈ V значение (charMonoidHom he hL w) v равно e(L(v,w)).

LaTeX

$$$\\text{charMonoidHom}(he,hL)(w)(v) = e\\bigl(L(v,w)\\bigr).$$$

Lean4

/-- Monoid homomorphism mapping `w` to `fun v ↦ e (L v w)`. -/
noncomputable def charMonoidHom (he : Continuous e) (hL : Continuous fun p : V × W ↦ L p.1 p.2) :
    Multiplicative W →* (V →ᵇ ℂ) where
  toFun w := char he hL w
  map_one' := char_zero_eq_one
  map_mul' := char_add_eq_mul (he := he) (hL := hL)

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