addHaar_reindex — Mathlib

English

For any basis b, the Haar measure b.addHaar assigns measure 1 to the parallelepiped spanned by b.

Русский

Для любого базиса b мера Хаара b.addHaar придаёт площади параллелепипеду, порождаемому b, единицу.

LaTeX

$$$b.addHaar( b.parallelepiped ) = 1$$$

Lean4

@[simp]
theorem addHaar_reindex (b : Basis ι ℝ E) (e : ι ≃ ι') : (b.reindex e).addHaar = b.addHaar := by
  rw [Basis.addHaar, b.parallelepiped_reindex e, ← Basis.addHaar]

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