Documentation Verification Report

Weight

📁 Source: Mathlib/Combinatorics/Quiver/Path/Weight.lean

Statistics

Metric	Count
Definitions `addWeight`, `addWeightOfEPs`, `weight`, `weightOfEPs`	4
Theorems `addWeightOfEPs_comp`, `addWeightOfEPs_cons`, `addWeightOfEPs_nil`, `addWeight_comp`, `addWeight_cons`, `addWeight_nil`, `weightOfEPs_comp`, `weightOfEPs_cons`, `weightOfEPs_nil`, `weightOfEPs_nonneg`, `weightOfEPs_pos`, `weight_comp`, `weight_cons`, `weight_nil`, `weight_nonneg`, `weight_pos`	16
Total	20

Quiver.Path

Definitions

Name	Category	Theorems
`addWeight` 📖	CompOp	3 math math: `addWeight_nil`, `addWeight_cons`, `addWeight_comp`
`addWeightOfEPs` 📖	CompOp	3 math math: `addWeightOfEPs_comp`, `addWeightOfEPs_nil`, `addWeightOfEPs_cons`
`weight` 📖	CompOp	5 math math: `weight_nonneg`, `weight_comp`, `weight_pos`, `weight_nil`, `weight_cons`
`weightOfEPs` 📖	CompOp	5 math math: `weightOfEPs_cons`, `weightOfEPs_pos`, `weightOfEPs_nonneg`, `weightOfEPs_comp`, `weightOfEPs_nil`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addWeightOfEPs_comp` 📖	mathematical	—	`addWeightOfEPs` `comp` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`addWeight_comp`
`addWeightOfEPs_cons` 📖	mathematical	—	`addWeightOfEPs` `cons` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`addWeight_cons`
`addWeightOfEPs_nil` 📖	mathematical	—	`addWeightOfEPs` `nil` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`addWeight_nil`
`addWeight_comp` 📖	mathematical	—	`addWeight` `comp` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`addWeight_nil` `add_zero` `addWeight_cons` `add_assoc`
`addWeight_cons` 📖	mathematical	—	`addWeight` `cons` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`addWeight.eq_2`
`addWeight_nil` 📖	mathematical	—	`addWeight` `nil` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`weightOfEPs_comp` 📖	mathematical	—	`weightOfEPs` `comp` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`weight_comp`
`weightOfEPs_cons` 📖	mathematical	—	`weightOfEPs` `cons` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`weight_cons`
`weightOfEPs_nil` 📖	mathematical	—	`weightOfEPs` `nil` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`weight_nil`
`weightOfEPs_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`weightOfEPs` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`weight_nonneg`
`weightOfEPs_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`weightOfEPs` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`weight_pos`
`weight_comp` 📖	mathematical	—	`weight` `comp` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`weight_nil` `mul_one` `weight_cons` `mul_assoc`
`weight_cons` 📖	mathematical	—	`weight` `cons` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`weight.eq_2`
`weight_nil` 📖	mathematical	—	`weight` `nil` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`weight_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`weight` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`weight_nil` `IsStrictOrderedRing.toZeroLEOneClass` `weight_cons` `mul_nonneg` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing`
`weight_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`weight` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`weight_nil` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `weight_cons` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono`

---

← Back to Index