Theorems · Definition · general algebraic systems

DFinsupp.coeFnAddMonoidHom

{ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddZeroClass (β i)] → (Π₀ (i : ι), β i) →+ (i : ι) → β i

Coercion from a DFinsupp to a pi type is an AddMonoidHom.

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

7 results in Mathlib

Foundations

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

Assumes

AddZeroClass