reindexLinearEquiv_refl_refl — Mathlib

English

The reindexLinearEquiv corresponding to identity on both indices is the identity linear equivalence.

Русский

Реиндексационная линейная эквивалентность для тождественных перестановок индексов равна тождественной линейной эквивалентности.

LaTeX

$$$ \mathrm{reindexLinearEquiv}\ R\ A\ (\mathrm{Equiv.refl}\ m)\ (\mathrm{Equiv.refl}\ n) = \mathrm{LinearEquiv.refl}\ R\ (\mathrm{Matrix}\ m n A). $$$

Lean4

@[simp]
theorem reindexLinearEquiv_refl_refl : reindexLinearEquiv R A (Equiv.refl m) (Equiv.refl n) = LinearEquiv.refl R _ :=
  LinearEquiv.ext fun _ => rfl

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