Fin

📁 Source: Mathlib/LinearAlgebra/Basis/Fin.lean

Statistics

Metric	Count
Definitions finTwoProd, mkFinCons, mkFinConsOfLE	3
Theorems coe_finTwoProd_repr, coe_mkFinCons, coe_mkFinConsOfLE, finTwoProd_one, finTwoProd_zero	5
Total	8

Module.Basis

Definitions

Name	Category	Theorems
finTwoProd 📖	CompOp	6 math math: Matrix.toLin_finTwoProd_apply, coe_finTwoProd_repr, Matrix.toLin_finTwoProd_toContinuousLinearMap, Matrix.toLin_finTwoProd, finTwoProd_zero, finTwoProd_one
mkFinCons 📖	CompOp	1 math math: coe_mkFinCons
mkFinConsOfLE 📖	CompOp	1 math math: coe_mkFinConsOfLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_finTwoProd_repr 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Prod.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.instAddCommMonoid Prod.instModule Semiring.toModule Finsupp.module EquivLike.toFunLike LinearEquiv.instEquivLike repr finTwoProd Matrix.vecCons Matrix.vecEmpty	—	RingHomInvPair.ids
coe_mkFinCons 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DFunLike.coe Module.Basis instFunLike mkFinCons Fin.cons Submodule.addCommMonoid Submodule.module	—	—
coe_mkFinConsOfLE 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.module instFunLike mkFinConsOfLE Fin.cons LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Submodule.inclusion	—	coe_mkFinCons
finTwoProd_one 📖	mathematical	—	DFunLike.coe Module.Basis Prod.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Prod.instModule Semiring.toModule instFunLike finTwoProd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids coe_ofEquivFun Pi.single_eq_of_ne Nat.instCharZero Nat.instAtLeastTwoHAddOfNat Pi.single_eq_same
finTwoProd_zero 📖	mathematical	—	DFunLike.coe Module.Basis Prod.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Prod.instModule Semiring.toModule instFunLike finTwoProd AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	RingHomInvPair.ids coe_ofEquivFun Pi.single_eq_same Pi.single_eq_of_ne Nat.instCharZero Nat.instAtLeastTwoHAddOfNat

---

← Back to Index