Theorems · Definition · linear algebra

Finsupp.lmapDomain

{α : Type u_1} →
  (M : Type u_2) →
    (R : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {α' : Type u_9} → (α → α') → (α →₀ M) →ₗ[R] α' →₀ M

Interpret Finsupp.mapDomain as a linear map.

Defined in

Mathlib.LinearAlgebra.Finsupp.Defs

Cited by

63 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModule