reindexLieEquiv_apply — Mathlib

English

The application of reindexLieEquiv to a matrix M equals the reindexed matrix: Matrix.reindexLieEquiv e M = Matrix.reindex e e M.

Русский

Применение reindexLieEquiv к матрице M даёт переставленную по e матрицу: Matrix.reindexLieEquiv e M = Matrix.reindex e e M.

LaTeX

$$$\\text{Matrix.reindexLieEquiv } e\,M = \\text{Matrix.reindex } e\,e\,M.$$$

Lean4

@[simp]
theorem reindexLieEquiv_apply (M : Matrix n n R) : Matrix.reindexLieEquiv e M = Matrix.reindex e e M :=
  rfl

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