Theorems · Definition · linear algebra

LinearMap.splittingOfFunOnFintypeSurjective

{R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {α : Type u_5} → [Finite α] → (f : M →ₗ[R] α → R) → Function.Surjective ⇑f → (α → R) →ₗ[R] M

A surjective linear map to functions on a finite type has a splitting.

Defined in

Mathlib.LinearAlgebra.Finsupp.Pi

Cited by

3 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleFinite