linearCombination_id_surjective — Mathlib

English

Finsupp.linearCombination with the identity map id: M→M is surjective.

Русский

Finsupp.linearCombination с тождественным отображением id: M→M является сюръективным.

LaTeX

$$Function.Surjective (linearCombination_R id).$$

Lean4

/-- Any module is a quotient of a free module. This is stated as surjectivity of
`Finsupp.linearCombination R id : (M →₀ R) →ₗ[R] M`. -/
theorem linearCombination_id_surjective (M) [AddCommMonoid M] [Module R M] :
    Function.Surjective (linearCombination R (id : M → M)) :=
  linearCombination_surjective R Function.surjective_id

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