fundamentalDomain_reindex — Mathlib

English

Reindexing the basis by a bijection e does not change the fundamental domain: fundamentalDomain(b.reindex e) = fundamentalDomain(b).

Русский

Переиндексация базиса по перестановке e не изменяет фундаментальную область: fundamentalDomain(b.reindex e) = fundamentalDomain(b).

LaTeX

$$$ \operatorname{fundamentalDomain}(b.reindex\,e) = \operatorname{fundamentalDomain}(b) $$$

Lean4

@[simp]
theorem fundamentalDomain_reindex {ι' : Type*} (e : ι ≃ ι') : fundamentalDomain (b.reindex e) = fundamentalDomain b :=
  by
  ext
  simp_rw [mem_fundamentalDomain, Basis.repr_reindex_apply]
  rw [Equiv.forall_congr' e]
  simp_rw [implies_true]

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