reindex_refl — Mathlib

English

A simp lemma stating symmetry of reindex in the dependent/unstated case.

Русский

Упрощенное леммное утверждение симметрии переиндексации в зависимом/неназначенном случае.

LaTeX

$$$@[simp] \\text{ reindex refl symmetric }$$$

Lean4

@[simp]
theorem reindex_refl : reindex R s (Equiv.refl ι) = LinearEquiv.refl R _ :=
  by
  apply LinearEquiv.toLinearMap_injective
  ext
  simp only [Equiv.refl_symm, Equiv.refl_apply, reindex, domDomCongrLinearEquiv', LinearEquiv.coe_symm_mk,
    LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe, LinearEquiv.refl_toLinearMap, LinearMap.id_coe, id_eq]
  simp

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