toMatrix_toPEquiv_apply — Mathlib

English

For a bijection f: m ≃. n and i, the matrix-to-equivalence mapping yields a matrix with a single 1 in the (i, f(i)) position and zeros elsewhere.

Русский

Для биекции f: m ≃. n и элемента i матрица-toPEquiv применится к единице и даст единицу в позиции (i, f(i)) и нули в остальных местах.

LaTeX

$$$f.toPEquiv.toMatrix_i = \\mathrm{Pi.single}(f(i), 1)$$$

Lean4

@[simp]
theorem toMatrix_toPEquiv_apply [DecidableEq n] [Zero α] [One α] (f : m ≃ n) (i) :
    f.toPEquiv.toMatrix i = Pi.single (f i) (1 : α) := by
  ext
  simp [toMatrix_apply, Pi.single_apply, eq_comm]

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