Theorems · Definition · linear algebra

FunOnFinite.map

{M : Type u_5} →
  [AddCommMonoid M] → {X : Type u_6} → {Y : Type u_7} → [Finite X] → [Finite Y] → (X → Y) → (X → M) → Y → M

The map (X → M) → (Y → M) induced by a map X → Y between finite types.

Defined in

Mathlib.LinearAlgebra.Finsupp.Pi

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddCommMonoidFiniteFinite