linearCombination_surjective — Mathlib

English

The map Finsupp.linearCombination is surjective for the differential D.

Русский

Отображение Finsupp.linearCombination сюрьективно относительно дифференциала D.

LaTeX

$$$\\text{Surjective}(\\mathrm{Finsupp.linearCombination}(S,\\mathrm{D}(R,S)))$$$

Lean4

theorem linearCombination_surjective : Function.Surjective (Finsupp.linearCombination S (KaehlerDifferential.D R S)) :=
  by rw [← LinearMap.range_eq_top, range_linearCombination, span_range_derivation]

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