leftInverse_splittingOfFinsuppSurjective

English

The splitting map is a left-inverse of the surjective map f, i.e., f ∘ splitting = id on α →₀ R.

Русский

Разложение является левым обратным к отображению f: f ∘ splitting = id на α →₀ R.

LaTeX

$$$LeftInverse\; f\; (splittingOfFinsuppSurjective\;f\;s)$$$

Lean4

theorem leftInverse_splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f) :
    LeftInverse f (splittingOfFinsuppSurjective f s) := fun g =>
  LinearMap.congr_fun (splittingOfFinsuppSurjective_splits f s) g

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