modularCharacter — Mathlib

English

The modular-character homomorphism is defined by modularCharacterFun and is a monoid homomorphism from G to the nonnegative reals.

Русский

Модульная характеристика образует гомоморфизм моноида от G к неотрицательному вещественному числу.

LaTeX

$$modularCharacter : G →* NNReal$$

Lean4

/-- The modular character homomorphism. The underlying function is `modularCharacterFun`, which is
`g ↦ μ (· * g⁻¹) / μ`, where `μ` is a left Haar measure.
-/
noncomputable def modularCharacter : G →* ℝ≥0
    where
  toFun := modularCharacterFun
  map_one' := modularCharacterFun_map_one
  map_mul' := modularCharacterFun_map_mul

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