repr_eq_iff — Mathlib

English

An unbundled version: given a function f, additive and scalar compatibilities hold, and f matches on basis vectors, then b.repr x i = f(x,i) for all x,i.

Русский

Необъединённая версия: при данной функции f, соблюдении аддитивности и совместимости скаляров, и при равенстве на базисных векторах, имеем b.repr x i = f(x,i) для всех x,i.

LaTeX

$$$$ b.repr\,x\,i = f\,x\,i $$$$

Lean4

theorem repr_eq_iff {b : Basis ι R M} {f : M →ₗ[R] ι →₀ R} : ↑b.repr = f ↔ ∀ i, f (b i) = Finsupp.single i 1 :=
  ⟨fun h i => h ▸ b.repr_self i, fun h => b.ext fun i => (b.repr_self i).trans (h i).symm⟩

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