modularCharacterFun_map_one

Mathlib.MeasureTheory.Group.ModularCharacter

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.modularCharacterFun_map_one

English

The modular-character map sends the identity to one: modularCharacterFun(1) = 1.

Русский

Модульная характеристика отображает единицу в единицу: modularCharacterFun(1) = 1.

LaTeX

$$modularCharacterFun(1) = 1$$

Lean4

@[to_additive]
theorem modularCharacterFun_map_one : modularCharacterFun (1 : G) = 1 := by
  simp [modularCharacterFun, haarScalarFactor_self]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru