toMatrix_apply — Mathlib

English

For any PEquiv f, the transpose of its toMatrix equals the toMatrix of f.symm, i.e., (f.toMatrix)ᵀ = (f.symm.toMatrix).

Русский

Для любого PEquiv f транспонированная матрица равно матрице обратной перестановки: f.toMatrixᵀ = f.symm.toMatrix.

LaTeX

$$$\\text{For } f,\\;(f.toMatrix)^{\\top} = f^{-1}.toMatrix.$$$

Lean4

@[simp]
theorem toMatrix_apply [DecidableEq n] [Zero α] [One α] (f : m ≃. n) (i j) :
    toMatrix f i j = if j ∈ f i then (1 : α) else 0 :=
  rfl

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