of_comp — Mathlib

English

If a linear map f is injective on the span of the range of v, then LinearIndepOn R (f ∘ v) s is equivalent to LinearIndepOn R v s.

Русский

Если линейное отображение f инъективно на замке порождаемых образов {v}, тогда LinearIndepOn R (f ∘ v) s эквивалентно LinearIndepOn R v s.

LaTeX

$$$\\\\mathrm{LinearIndepOn}_R (f \\circ v) s \\\\iff \\\\mathrm{LinearIndepOn}_R v s \\\\text{ whenever } \\\\mathrm{InjOn} (LinearMap.instFunLike.coe f) (\\\\operatorname{span} R (\\\\operatorname{range} v)).$$$

Lean4

theorem of_comp (f : M →ₗ[R] M') (hfv : LinearIndepOn R (f ∘ v) s) : LinearIndepOn R v s :=
  LinearIndependent.of_comp f hfv

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