Theorems · Definition · linear algebra

Finsupp.uniqueLinearEquiv

(R : Type u_1) →
  {α : Type u_3} →
    (M : Type u_4) →
      [inst : AddCommMonoid M] → [inst_1 : Semiring R] → [inst_2 : Module R M] → [Subsingleton α] → α → (α →₀ M) ≃ₗ[R] M

If α has a unique term, then the type of finitely supported functions α →₀ M is R-linearly equivalent to M.

Defined in

Mathlib.LinearAlgebra.Finsupp.Pi

Cited by

16 results in Mathlib

Foundations

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

Assumes

AddCommMonoidSemiringModuleSubsingleton