exists_fin' — Mathlib

English

For any finite module M over R, there exists a natural number n and a surjective linear map f: (Fin n → R) → M.

Русский

Для любого конечного модуля M над R существует натуральное n и сюръективное линейное отображение f: (Fin n → R) → M.

LaTeX

$$$\\forall [Module.Finite R M], \\exists n (f : (Fin n \to R) \to_\\!{R} M), Surjective f.$$$

Lean4

/-- A finite module admits a surjective linear map from a finite free module. -/
theorem exists_fin' [Module.Finite R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Surjective f :=
  have ⟨n, f, hf⟩ := (Submodule.fg_iff_exists_fin_linearMap R M).mp fg_top
  ⟨n, f, by rw [← LinearMap.range_eq_top, hf]⟩

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