repr_range — Mathlib

English

If M is a nontrivial module, then a basis b of M has at least one nonzero basis vector; i.e., there exists i with b i ≠ 0.

Русский

Если модуль M ненулевой, то базис b модуля M содержит как минимум один ненулевой вектор; то есть существует индекс i, такой что b i ≠ 0.

LaTeX

$$$\exists i,\ b(i) \neq 0.$$$

Lean4

theorem repr_range : LinearMap.range (b.repr : M →ₗ[R] ι →₀ R) = Finsupp.supported R R univ := by
  rw [LinearEquiv.range, Finsupp.supported_univ]

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