Documentation Verification Report

Pi

📁 Source: Mathlib/LinearAlgebra/Multilinear/Pi.lean

Statistics

Metric	Count
Definitions `piFamily`, `piFamilyₗ`	2
Theorems `piFamily_add`, `piFamily_apply`, `piFamily_compLinearMap_lsingle`, `piFamily_single`, `piFamily_single_left`, `piFamily_single_left_apply`, `piFamily_smul`, `piFamily_zero`, `piFamilyₗ_apply`, `pi_ext`, `pi_ext_iff`	11
Total	13

MultilinearMap

Definitions

Name	Category	Theorems
`piFamily` 📖	CompOp	9 math math: `piFamily_add`, `piFamily_apply`, `piFamilyₗ_apply`, `piFamily_single_left_apply`, `piFamily_single_left`, `piFamily_smul`, `piFamily_single`, `piFamily_compLinearMap_lsingle`, `piFamily_zero`
`piFamilyₗ` 📖	CompOp	1 math math: `piFamilyₗ_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`piFamily_add` 📖	mathematical	—	`piFamily` `Pi.instAdd` `MultilinearMap` `instAdd` `Pi.addCommMonoid` `Pi.module`	—	`ext`
`piFamily_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `Pi.addCommMonoid` `Pi.module` `instFunLikeForall` `piFamily`	—	—
`piFamily_compLinearMap_lsingle` 📖	mathematical	—	`compLinearMap` `Pi.addCommMonoid` `Pi.module` `piFamily` `LinearMap.single` `LinearMap.compMultilinearMap` `Fintype.decidablePiFintype`	—	`ext` `piFamily_single`
`piFamily_single` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `Pi.addCommMonoid` `Pi.module` `instFunLikeForall` `piFamily` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Fintype.decidablePiFintype`	—	`eq_or_ne` `Pi.single_eq_same` `Pi.single_eq_of_ne'` `Function.ne_iff` `map_coord_zero`
`piFamily_single_left` 📖	mathematical	—	`piFamily` `Pi.single` `MultilinearMap` `instZero` `Fintype.decidablePiFintype` `LinearMap.compMultilinearMap` `Pi.addCommMonoid` `Pi.module` `LinearMap.single` `compLinearMap` `LinearMap.proj`	—	`ext` `piFamily_single_left_apply`
`piFamily_single_left_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `Pi.addCommMonoid` `Pi.module` `instFunLikeForall` `piFamily` `Pi.single` `instZero` `Fintype.decidablePiFintype` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`eq_or_ne` `Pi.single_eq_same` `Pi.single_eq_of_ne'`
`piFamily_smul` 📖	mathematical	`SMulCommClass` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`piFamily` `Pi.instSMul` `MultilinearMap` `instSMul` `Pi.addCommMonoid` `Pi.module` `Pi.distribSMul` `Pi.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`ext` `Pi.smulCommClass`
`piFamily_zero` 📖	mathematical	—	`piFamily` `Pi.instZero` `MultilinearMap` `instZero` `Pi.addCommMonoid` `Pi.module`	—	`ext`
`piFamilyₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MultilinearMap` `Pi.addCommMonoid` `Pi.module` `addCommMonoid` `instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Pi.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `LinearMap.instFunLike` `piFamilyₗ` `piFamily`	—	`smulCommClass_self` `Pi.smulCommClass`
`pi_ext` 📖	—	`Finite` `compLinearMap` `Pi.addCommMonoid` `Pi.module` `LinearMap.single`	—	—	`ext` `nonempty_fintype` `Finset.univ_sum_single` `map_sum_finset` `Finset.sum_congr`
`pi_ext_iff` 📖	mathematical	`Finite`	`compLinearMap` `Pi.addCommMonoid` `Pi.module` `LinearMap.single`	—	`pi_ext`

---

← Back to Index