Theorems · Definition · group theory

Finsupp.mapRange.addEquiv

{ι : Type u_1} →
  {M : Type u_3} →
    {N : Type u_4} → [inst : AddCommMonoid M] → [inst_1 : AddCommMonoid N] → M ≃+ N → (ι →₀ M) ≃+ (ι →₀ N)

Finsupp.mapRange.AddMonoidHom as an equiv.

Defined in

Mathlib.Algebra.Group.Finsupp

Cited by

15 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoid