modularCharacterFun_pos — Mathlib

English

The modular-character map respects multiplication: modularCharacterFun (g h) = modularCharacterFun g · modularCharacterFun h.

Русский

Модульная характеристика корректно ведёт себя под умножением: modularCharacterFun (gh) = modularCharacterFun g · modularCharacterFun h.

LaTeX

$$modularCharacterFun (gh) = modularCharacterFun g \\cdot modularCharacterFun h$$

Lean4

@[to_additive]
theorem modularCharacterFun_pos (g : G) : 0 < modularCharacterFun g :=
  by
  borelize G
  rw [modularCharacterFun_eq_haarScalarFactor MeasureTheory.Measure.haar g]
  exact haarScalarFactor_pos_of_isHaarMeasure _ _

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