Theorems · Theorem · linear algebra

DFinsupp.mker_mapRangeAddMonoidHom

∀ {ι : Type u_1} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [inst : (i : ι) → AddCommMonoid (β₁ i)]
  [inst_1 : (i : ι) → AddCommMonoid (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i),
  AddMonoidHom.mker (DFinsupp.mapRange.addMonoidHom f) =
    AddSubmonoid.comap DFinsupp.coeFnAddMonoidHom (AddSubmonoid.pi Set.univ fun i => AddMonoidHom.mker (f i))

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoid