equivFun_self — Mathlib

English

If B is a basis with finite index, then for all i, j we have b.equivFun (b i) j = 1 if i = j and 0 otherwise.

Русский

Пусть B — база с конечным индексом; тогда для любых индексов i, j выполняется b.equivFun (b i) j = 1, если i = j, и 0, если i ≠ j.

LaTeX

$$$$ b.equivFun\,(b_i)\,j = \begin{cases}1 & \text{если } i=j \\ 0 & \text{иначе} \end{cases} $$$$

Lean4

@[simp]
theorem equivFun_self [Finite ι] [DecidableEq ι] (b : Basis ι R M) (i j : ι) :
    b.equivFun (b i) j = if i = j then 1 else 0 := by rw [b.equivFun_apply, b.repr_self_apply]

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