range_codRestrict — Mathlib

English

If M is finite and f: M →ₛₗ[τ₁₂] M₂ is surjective on the scalars, then the range of f is finite.

Русский

Если область определения M конечна и f линейно отображает M в M₂ (при сюръективных скалярах), то диапазон f конечно по количеству элементов.

LaTeX

$$$\text{Fintype } M \Rightarrow \operatorname{Fintype}(\operatorname{range} f)$$$

Lean4

theorem range_codRestrict {τ₂₁ : R₂ →+* R} [RingHomSurjective τ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf) :
    range (codRestrict p f hf) = comap p.subtype (LinearMap.range f) := by
  simpa only [range_eq_map] using map_codRestrict _ _ _ _

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