Theorems · Definition · linear algebra

Finsupp.linearEquivFunOnFinite

(R : Type u_9) →
  (M : Type u_11) →
    (α : Type u_12) →
      [Finite α] → [inst : AddCommMonoid M] → [inst_1 : Semiring R] → [inst_2 : Module R M] → (α →₀ M) ≃ₗ[R] α → M

Given Finite α, linearEquivFunOnFinite R is the natural R-linear equivalence between α →₀ β and α → β.

Defined in

Mathlib.LinearAlgebra.Finsupp.Defs

Cited by

28 results in Mathlib

Foundations

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

Assumes

FiniteAddCommMonoidSemiringModule