map_toMatrix — Mathlib

English

For any permutation σ, applying a ring homomorphism f entrywise to σ.toMatrix leaves the matrix unchanged, since its entries are only 0 or 1.

Русский

Для любой перестановки σ применение кольцевого гомоморфа f поэлементно к σ.toMatrix оставляет матрицу неизменной, поскольку её элементы равны 0 или 1.

LaTeX

$$$\\sigma.toPEquiv.toMatrix.map f = \\sigma.toPEquiv.toMatrix$$$

Lean4

@[simp]
theorem map_toMatrix [DecidableEq n] [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (σ : m ≃. n) :
    σ.toMatrix.map f = σ.toMatrix := by
  ext i j
  simp

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