Fin

📁 Source: Mathlib/Algebra/BigOperators/Finsupp/Fin.lean

Statistics

Metric	Count
Definitions finTwoArrowEquiv'	1
Theorems ofSupportFinite_fin_two_eq, sum_cons, sum_cons', finTwoArrowEquiv'_apply, finTwoArrowEquiv'_sum_eq, finTwoArrowEquiv'_symm_apply	6
Total	7

Finsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofSupportFinite_fin_two_eq 📖	mathematical	—	ofSupportFinite MulZeroClass.toZero Nat.instMulZeroClass Matrix.vecCons DFunLike.coe Finsupp instFunLike Matrix.vecEmpty Set.toFinite Function.support Subtype.finite Finite.of_fintype Fin.fintype Set Set.instMembership	—	Set.toFinite Subtype.finite Finite.of_fintype ext_iff
sum_cons 📖	mathematical	—	sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid cons AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	sum_fintype Fin.sum_cons
sum_cons' 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	sum cons AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Fin.tail	—	sum_fintype Fin.sum_univ_succ Finset.sum_congr

(root)

Definitions

Name	Category	Theorems
finTwoArrowEquiv' 📖	CompOp	3 math math: finTwoArrowEquiv'_apply, finTwoArrowEquiv'_symm_apply, finTwoArrowEquiv'_sum_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finTwoArrowEquiv'_apply 📖	mathematical	—	DFunLike.coe Equiv Finsupp EquivLike.toFunLike Equiv.instEquivLike finTwoArrowEquiv' Finsupp.instFunLike	—	—
finTwoArrowEquiv'_sum_eq 📖	mathematical	—	Finsupp.sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe Equiv Finsupp EquivLike.toFunLike Equiv.instEquivLike Equiv.symm finTwoArrowEquiv' AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Finite.of_fintype Finsupp.equivFunOnFinite_symm_sum Finset.sum_congr Fin.sum_univ_two Matrix.cons_val_fin_one
finTwoArrowEquiv'_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Finsupp EquivLike.toFunLike Equiv.instEquivLike Equiv.symm finTwoArrowEquiv' Finsupp.equivFunOnFinite Matrix.vecCons Matrix.vecEmpty	—	—

---

← Back to Index