basisOf_reindex — Mathlib

English

Equality of a basis with its explicit Basis.mk description using vsub coordinates.

Русский

Согласование между базисом и явным описанием Basis.mk через vsub координаты.

LaTeX

$$b.basisOf i = Basis.mk ... (describing vectors as b_j −ᵥ b_i)$$

Lean4

@[simp]
theorem basisOf_reindex (i : ι') :
    (b.reindex e).basisOf i = (b.basisOf <| e.symm i).reindex (e.subtypeEquiv fun _ => e.eq_symm_apply.not) :=
  by
  ext j
  simp

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