Documentation Verification Report

DomCoprod

📁 Source: Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

Statistics

Metric	Count
Definitions `domCoprod`, `domCoprod'`, `summand`, `ModSumCongr`	4
Theorems `domCoprod'_apply`, `summand_add_swap_smul_eq_zero`, `summand_eq_zero_of_smul_invariant`, `summand_mk''`, `domCoprod_apply`, `domCoprod_coe`, `domCoprod_alternization`, `domCoprod_alternization_coe`, `domCoprod_alternization_eq`	9
Total	13

AlternatingMap

Definitions

Name	Category	Theorems
`domCoprod` 📖	CompOp	5 math math: `domCoprod_coe`, `MultilinearMap.domCoprod_alternization_eq`, `domCoprod'_apply`, `MultilinearMap.domCoprod_alternization`, `domCoprod_apply`
`domCoprod'` 📖	CompOp	1 math math: `domCoprod'_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`domCoprod'_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `AlternatingMap` `AddCommGroup.toAddCommMonoid` `instAddCommMonoid` `instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearMap.instFunLike` `domCoprod'` `TensorProduct.tmul` `domCoprod`	—	`smulCommClass_self` `TensorProduct.smulCommClass_left`
`domCoprod_apply` 📖	mathematical	—	`DFunLike.coe` `AlternatingMap` `CommSemiring.toSemiring` `TensorProduct` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLike` `domCoprod` `MultilinearMap` `MultilinearMap.instFunLikeForall` `Finset.sum` `Equiv.Perm.ModSumCongr` `MultilinearMap.addCommMonoid` `Finset.univ` `QuotientGroup.fintype` `Equiv.Perm` `Equiv.Perm.permGroup` `Equiv.instFintype` `instFintypeSum` `MonoidHom.range` `Prod.instGroup` `Equiv.Perm.sumCongrHom` `QuotientGroup.leftRelDecidable` `MonoidHom.decidableMemRange` `instFintypeProd` `Fintype.decidableEqEquivFintype` `domCoprod.summand`	—	—
`domCoprod_coe` 📖	mathematical	—	`toMultilinearMap` `CommSemiring.toSemiring` `TensorProduct` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `domCoprod` `Finset.sum` `Equiv.Perm.ModSumCongr` `MultilinearMap` `MultilinearMap.addCommMonoid` `Finset.univ` `QuotientGroup.fintype` `Equiv.Perm` `Equiv.Perm.permGroup` `Equiv.instFintype` `instFintypeSum` `MonoidHom.range` `Prod.instGroup` `Equiv.Perm.sumCongrHom` `QuotientGroup.leftRelDecidable` `MonoidHom.decidableMemRange` `instFintypeProd` `Fintype.decidableEqEquivFintype` `domCoprod.summand`	—	`MultilinearMap.ext`

AlternatingMap.domCoprod

Definitions

Name	Category	Theorems
`summand` 📖	CompOp	5 math math: `summand_mk''`, `AlternatingMap.domCoprod_coe`, `summand_eq_zero_of_smul_invariant`, `AlternatingMap.domCoprod_apply`, `summand_add_swap_smul_eq_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`summand_add_swap_smul_eq_zero` 📖	mathematical	—	`TensorProduct` `AddCommGroup.toAddCommMonoid` `TensorProduct.add` `DFunLike.coe` `MultilinearMap` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `MultilinearMap.instFunLikeForall` `summand` `Equiv.Perm` `Equiv.Perm.ModSumCongr` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MulAction.toSemigroupAction` `MulAction.quotient` `Monoid.toMulAction` `MonoidHom.range` `Prod.instGroup` `Equiv.Perm.sumCongrHom` `MulAction.left_quotientAction` `Equiv.swap` `TensorProduct.zero`	—	`Quotient.inductionOn'` `MulAction.left_quotientAction` `smul_eq_mul` `Equiv.Perm.sign_mul` `Equiv.Perm.sign_swap` `AddGroup.int_smulCommClass'` `neg_mul` `one_mul` `Units.neg_smul` `Equiv.apply_swap_eq_self` `add_neg_cancel`
`summand_eq_zero_of_smul_invariant` 📖	mathematical	`Equiv.Perm` `Equiv.Perm.ModSumCongr` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MulAction.toSemigroupAction` `MulAction.quotient` `Monoid.toMulAction` `MonoidHom.range` `Prod.instGroup` `Equiv.Perm.sumCongrHom` `MulAction.left_quotientAction` `Equiv.swap`	`DFunLike.coe` `MultilinearMap` `TensorProduct` `AddCommGroup.toAddCommMonoid` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `MultilinearMap.instFunLikeForall` `summand` `TensorProduct.zero`	—	`Quotient.inductionOn'` `MulAction.left_quotientAction` `AddGroup.int_smulCommClass'` `QuotientGroup.leftRel_apply` `Quotient.exact'` `AlternatingMap.map_eq_zero_of_eq` `TensorProduct.zero_tmul` `smul_zero` `Equiv.Perm.inv_eq_iff_eq` `mul_inv_rev` `Equiv.swap_apply_left` `Equiv.symm_apply_apply` `Equiv.congr_fun` `TensorProduct.tmul_zero`
`summand_mk''` 📖	mathematical	—	`summand` `Quotient.mk''` `Equiv.Perm` `QuotientGroup.leftRel` `Equiv.Perm.permGroup` `MonoidHom.range` `Prod.instGroup` `Equiv.Perm.sumCongrHom` `Units` `Int.instMonoid` `MultilinearMap` `TensorProduct` `AddCommGroup.toAddCommMonoid` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `MultilinearMap.instAddCommGroup` `TensorProduct.addCommGroup` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Units.instMulOneClass` `MonoidHom.instFunLike` `Equiv.Perm.sign` `instFintypeSum` `MultilinearMap.domDomCongr` `MultilinearMap.domCoprod` `AlternatingMap.toMultilinearMap`	—	—

Equiv.Perm

Definitions

Name	Category	Theorems
`ModSumCongr` 📖	CompOp	3 math math: `AlternatingMap.domCoprod_coe`, `AlternatingMap.domCoprod_apply`, `AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero`

MultilinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`domCoprod_alternization` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MultilinearMap` `TensorProduct` `AddCommGroup.toAddCommMonoid` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `TensorProduct.instModule` `AlternatingMap` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `AlternatingMap.instAddCommGroup` `AddMonoidHom.instFunLike` `alternatization` `instFintypeSum` `domCoprod` `AlternatingMap.domCoprod`	—	`AlternatingMap.coe_multilinearMap_injective` `AlternatingMap.domCoprod_coe` `alternatization_coe` `Finset.sum_partition` `Quotient.inductionOn'` `Finset.sum_congr` `Finset.filter.congr_simp` `Finset.map_univ_equiv` `Finset.filter_map` `Finset.sum_map` `mul_inv_rev` `inv_mul_cancel_right` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass` `Equiv.Perm.sign_mul` `Finset.univ_filter_exists` `Finset.sum_image` `Function.Injective.injOn` `Equiv.Perm.sumCongrHom_injective` `Equiv.Perm.sign_sumCongr` `SemigroupAction.mul_smul` `map_zsmul_unit` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `AddGroup.int_smulCommClass'` `domCoprod_alternization_coe` `map_sum` `Finset.smul_sum`
`domCoprod_alternization_coe` 📖	mathematical	—	`domCoprod` `AddCommGroup.toAddCommMonoid` `AlternatingMap.toMultilinearMap` `CommSemiring.toSemiring` `DFunLike.coe` `AddMonoidHom` `MultilinearMap` `AlternatingMap` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `AlternatingMap.instAddCommGroup` `AddMonoidHom.instFunLike` `alternatization` `Finset.sum` `Equiv.Perm` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `addCommMonoid` `Finset.univ` `Equiv.instFintype` `Units` `Int.instMonoid` `Units.instSMul` `SubNegMonoid.toZSMul` `TensorProduct.addCommGroup` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `Equiv.Perm.sign` `domDomCongr`	—	`smulCommClass_self` `TensorProduct.smulCommClass_left` `Finset.sum_congr` `alternatization_coe` `TensorProduct.sum_tmul` `TensorProduct.tmul_sum` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `AddGroup.int_smulCommClass'` `Units.smulCommClass_right` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.unit` `TensorProduct.CompatibleSMul.int`
`domCoprod_alternization_eq` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MultilinearMap` `TensorProduct` `AddCommGroup.toAddCommMonoid` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `TensorProduct.instModule` `AlternatingMap` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `AlternatingMap.instAddCommGroup` `AddMonoidHom.instFunLike` `alternatization` `instFintypeSum` `domCoprod` `AlternatingMap.toMultilinearMap` `TensorProduct.addCommMonoid` `AddMonoid.toNatSMul` `Nat.factorial` `Fintype.card` `AlternatingMap.domCoprod`	—	`domCoprod_alternization` `AlternatingMap.coe_alternatization` `SemigroupAction.mul_smul` `smulCommClass_self` `TensorProduct.smulCommClass_left` `AlternatingMap.domCoprod'_apply` `AddMonoid.nat_smulCommClass'` `TensorProduct.smul_tmul'` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower` `AddCommMonoid.nat_isScalarTower` `LinearMap.map_smul_of_tower` `LinearMap.IsScalarTower.compatibleSMul`

---

← Back to Index