coe_basis — Mathlib

English

The coercion of h.basis to a function matches e; i.e., (Module.Basis.instFunLike.coe h.basis) = e.

Русский

Преобразование h.basis в функцию совпадает с e; то есть коebasis equals e.

LaTeX

$$$ (Module.Basis.instFunLike.coe h.basis) = e $$$

Lean4

@[simp]
theorem coe_basis : ⇑h.basis = e := by
  ext i
  rw [Basis.apply_eq_iff]
  ext j
  rcases eq_or_ne i j with rfl | hne
  · simp [h.eval_same]
  · simp [hne, h.eval_of_ne hne.symm]

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