Finsupp

📁 Source: Mathlib/Algebra/DirectSum/Finsupp.lean

Statistics

Metric	Count
Definitions finsuppLEquivDirectSum	1
Theorems finsuppLEquivDirectSum_apply, finsuppLEquivDirectSum_single, finsuppLEquivDirectSum_symm_lof, lmap_finsuppLEquivDirectSum_eq	4
Total	5

(root)

Definitions

Name	Category	Theorems
finsuppLEquivDirectSum 📖	CompOp	4 math math: finsuppLEquivDirectSum_single, finsuppLEquivDirectSum_apply, lmap_finsuppLEquivDirectSum_eq, finsuppLEquivDirectSum_symm_lof

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finsuppLEquivDirectSum_apply 📖	mathematical	—	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp DirectSum Finsupp.instAddCommMonoid instAddCommMonoidDirectSum Finsupp.module DirectSum.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppLEquivDirectSum Finsupp.instFunLike	—	RingHomInvPair.ids
finsuppLEquivDirectSum_single 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DirectSum Finsupp.instAddCommMonoid instAddCommMonoidDirectSum Finsupp.module DirectSum.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppLEquivDirectSum Finsupp.single LinearMap LinearMap.instFunLike DirectSum.lof	—	Finsupp.toDFinsupp_single
finsuppLEquivDirectSum_symm_lof 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DirectSum Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum Finsupp.instAddCommMonoid DirectSum.instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm finsuppLEquivDirectSum LinearMap LinearMap.instFunLike DirectSum.lof Finsupp.single	—	DFinsupp.toFinsupp_single
lmap_finsuppLEquivDirectSum_eq 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum DirectSum.instModule LinearMap.instFunLike DirectSum.lmap LinearEquiv RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppLEquivDirectSum Finsupp.mapRange LinearMap.map_zero	—	DirectSum.ext RingHomInvPair.ids LinearMap.map_zero

---

← Back to Index