repr_eq_iff' — Mathlib

English

A variant of repr_eq' giving equivalence characterizations via a linear equivalence and its action on basis vectors.

Русский

Вариант repr_eq' с характеристикой эквивалентности через линейное соответствие и его действие на базисные векторы.

LaTeX

$$$$ b.repr = f \iff \forall i, f(b_i) = Finsupp.single i 1 $$$$

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⟩

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