mul_toMatrix_apply — Mathlib

English

The bottom element of the PEquiv has a zero matrix via toMatrix.

Русский

Нижний элемент PEquiv отображается в нулевую матрицу через toMatrix.

LaTeX

$$$\\text{toMatrix}(\\bot)^=0$$$

Lean4

theorem mul_toMatrix_apply [Fintype m] [NonAssocSemiring α] [DecidableEq n] (M : Matrix l m α) (f : m ≃. n) (i j) :
    (M * f.toMatrix :) i j = Option.casesOn (f.symm j) 0 (M i) :=
  by
  dsimp [Matrix.mul_apply, toMatrix_apply]
  rcases h : f.symm j with - | fj
  · simp [h, ← f.eq_some_iff]
  · rw [Finset.sum_eq_single fj]
    · simp [h, ← f.eq_some_iff]
    · rintro b - n
      simp [h, ← f.eq_some_iff, n.symm]
    · simp

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