Theorems · Theorem · ring theory

AddMonoidAlgebra.coeff_mapDomainAddEquiv

∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Add M] [inst_2 : Add N] (e : M ≃ N)
  (x : AddMonoidAlgebra R M), ((AddMonoidAlgebra.mapDomainAddEquiv R e) x).coeff = Finsupp.equivMapDomain e x.coeff

Defined in

Mathlib.Algebra.MonoidAlgebra.MapDomain

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddAdd