Mathlib Map

Theorems · Theorem · general algebraic systems

Finsupp.mapDomain_id

∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {v : α →₀ M}, Finsupp.mapDomain id v = v
Defined in
Mathlib.Data.Finsupp.Basic
Cited by
13 results in Mathlib
Foundations
Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Finsupp.lmapDomain_id · cited by 5Finsupp.lmapDomain_idModule.finitePresentation_of_free_of_surjective · cited by 3Module.finitePresentation…Convexity.StdSimplex.map_id · cited by 2StdSimplex.map_idFinsupp.lmapDomain_supported · cited by 2Finsupp.lmapDomain_suppor…MvPowerSeries.rename_id · cited by 2MvPowerSeries.rename_idFinsupp.mapDomain.addMonoidHom_id · cited by 1mapDomain.addMonoidHom_idAddMonoidAlgebra.mapDomainBialgHom_id · cited by 1AddMonoidAlgebra.mapDomai…Finsupp.mapDomain_surjective · cited by 1Finsupp.mapDomain_surject…groupHomology.H1CoresCoinfOfTrivial_exact · cited by 1groupHomology.H1CoresCoin…FunOnFinite.map_id · cited by 0FunOnFinite.map_idMonoidAlgebra.mapDomainBialgHom_id · cited by 0MonoidAlgebra.mapDomainBi…AddMonoidAlgebra.mapDomainNonUnitalRingHom_id · cited by 0AddMonoidAlgebra.mapDomai…MonoidAlgebra.mapDomainNonUnitalRingHom_id · cited by 0MonoidAlgebra.mapDomainNo…AddCommMonoid · cited by 12281AddCommMonoidFinsupp · cited by 5255FinsuppFinsupp.mapDomain · cited by 168Finsupp.mapDomainFinsupp.sum_single · cited by 19Finsupp.sum_singleFinsupp.mapDomain_idCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by13

Results whose statement or proof uses this declaration.