isAddHaarMeasure_basis_addHaar — Mathlib

English

For any basis b of a real vector space E, the measure b.addHaar is a Haar measure on E (i.e., left-invariant).

Русский

Для любого базиса b вещественного пространства E мера b.addHaar является мерой Хаара на E (левая инвариантность).

LaTeX

$$$IsAddHaarMeasure(b.addHaar)$$$

Lean4

instance _root_.isAddHaarMeasure_basis_addHaar (b : Basis ι ℝ E) : IsAddHaarMeasure b.addHaar := by rw [Basis.addHaar];
  exact Measure.isAddHaarMeasure_addHaarMeasure _

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