parallelepiped_reindex — Mathlib

English

Applying a linear map to the parallelepiped of a basis yields the parallelepiped of the mapped basis.

Русский

Применение линейного отображения к параллелепипеду базиса дает параллелепипед образованной базы.

LaTeX

$$$ \\mathrm{parallelepiped}(f\\circ v) = f''\\mathrm{parallelepiped}(v).$$$

Lean4

@[simp]
theorem parallelepiped_reindex (b : Basis ι ℝ E) (e : ι ≃ ι') : (b.reindex e).parallelepiped = b.parallelepiped :=
  PositiveCompacts.ext <| (congr_arg _root_.parallelepiped (b.coe_reindex e)).trans (parallelepiped_comp_equiv b e.symm)

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