distribHaarChar_pos

Mathlib.MeasureTheory.Measure.Haar.DistribChar

URI: https://scilib.ai/kg/mathlib#MeasureTheory.distribHaarChar_pos

English

For every g in G, the Haar character Δ(g) is strictly positive.

Русский

Для любого элемента g группы G значение характерa Хаара Δ(g) строго положительно.

LaTeX

$$$0 < \\Delta(g) \\quad \\text{для всех } g \\in G.$$

Lean4

theorem distribHaarChar_pos : 0 < distribHaarChar A g :=
  pos_iff_ne_zero.mpr ((Group.isUnit g).map (distribHaarChar A)).ne_zero

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

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

Разделы

Аффилиация

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