vecMul_toMatrix_toPEquiv — Mathlib

English

The vecMul under PEquiv corresponds to Function.comp with the inverse equivalence.

Русский

vecMul в PEquiv соответствует Function.comp с обратной эквивалентностью.

LaTeX

$$$ a ᵥ* σ.toPEquiv.toMatrix = a ∘ σ^{-1}$$$

Lean4

theorem vecMul_toMatrix_toPEquiv [DecidableEq n] [Fintype m] [NonAssocSemiring α] (σ : m ≃ n) (a : m → α) :
    a ᵥ* σ.toPEquiv.toMatrix = a ∘ σ.symm := by
  classical
  ext j
  simp [toMatrix, σ.apply_eq_iff_eq_symm_apply, vecMul, dotProduct]

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