addHaar_self — Mathlib

English

If you reindex a basis by a permutation equivalence, the associated Haar measure remains unchanged: the Haar measure is invariant under reindexing.

Русский

Если переставить индексы базиса по эквивалентности перестановки, соответствующая мера Хаара не меняется: она устойчива к перенумерации.

LaTeX

$$$(b.reindex\, e).addHaar = b.addHaar$$$

Lean4

theorem addHaar_self (b : Basis ι ℝ E) : b.addHaar (_root_.parallelepiped b) = 1 := by rw [Basis.addHaar];
  exact addHaarMeasure_self

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