Finsupp

📁 Source: Mathlib/LinearAlgebra/PiTensorProduct/Finsupp.lean

Statistics

Metric	Count
Definitions ofFinsuppEquiv, ofFinsuppEquiv'	2
Theorems ofFinsuppEquiv'_apply_apply, ofFinsuppEquiv'_tprod_single, ofFinsuppEquiv_apply, ofFinsuppEquiv_symm_single_tprod, ofFinsuppEquiv_tprod_single	5
Total	7

PiTensorProduct

Definitions

Name	Category	Theorems
ofFinsuppEquiv 📖	CompOp	3 math math: ofFinsuppEquiv_tprod_single, ofFinsuppEquiv_symm_single_tprod, ofFinsuppEquiv_apply
ofFinsuppEquiv' 📖	CompOp	2 math math: ofFinsuppEquiv'_tprod_single, ofFinsuppEquiv'_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofFinsuppEquiv'_apply_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids PiTensorProduct Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule instAddCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv ofFinsuppEquiv' MultilinearMap MultilinearMap.instFunLikeForall tprod Finset.prod CommSemiring.toCommMonoid Finset.univ	—	RingHomInvPair.ids ofFinsuppEquiv_apply constantBaseRingEquiv_tprod
ofFinsuppEquiv'_tprod_single 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule instAddCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv ofFinsuppEquiv' MultilinearMap MultilinearMap.instFunLikeForall tprod Finsupp.single Finset.prod CommSemiring.toCommMonoid Finset.univ	—	RingHomInvPair.ids ofFinsuppEquiv_tprod_single Finsupp.lcongr_single constantBaseRingEquiv_tprod
ofFinsuppEquiv_apply 📖	mathematical	—	DFunLike.coe Finsupp PiTensorProduct AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid Finsupp.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv ofFinsuppEquiv MultilinearMap MultilinearMap.instFunLikeForall tprod	—	RingHomInvPair.ids congr_tprod ofDFinsuppEquiv_tprod_apply
ofFinsuppEquiv_symm_single_tprod 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp PiTensorProduct AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid Finsupp.instAddCommMonoid Finsupp.module instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm ofFinsuppEquiv Finsupp.single MultilinearMap MultilinearMap.instFunLikeForall tprod	—	RingHomInvPair.ids LinearEquiv.symm_apply_eq ofFinsuppEquiv_tprod_single
ofFinsuppEquiv_tprod_single 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiTensorProduct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module instAddCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv ofFinsuppEquiv MultilinearMap MultilinearMap.instFunLikeForall tprod Finsupp.single	—	RingHomInvPair.ids congr_tprod Finsupp.toDFinsupp_single ofDFinsuppEquiv_tprod_single DFinsupp.toFinsupp_single

---

← Back to Index