Holor

Statistics

Metric	Count
Definitions `Holor`, `CPRankMax`, `CPRankMax1`, `assocLeft`, `assocRight`, `cprank`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instAddCommSemigroup`, `instAddGroup`, `instAddMonoid`, `instAddSemigroup`, `instInhabited`, `instModule`, `instNeg`, `instSMulOfMul`, `instZero`, `mul`, `slice`, `unitVec`, `HolorIndex`, `assocLeft`, `assocRight`, `drop`, `take`	26
Theorems `cast_type`, `cprankMax_1`, `cprankMax_add`, `cprankMax_mul`, `cprankMax_nil`, `cprankMax_sum`, `cprankMax_upper_bound`, `cprank_upper_bound`, `holor_index_cons_decomp`, `mul_assoc`, `mul_assoc0`, `mul_left_distrib`, `mul_right_distrib`, `mul_scalar_mul`, `mul_zero`, `slice_add`, `slice_eq`, `slice_sum`, `slice_unitVec_mul`, `slice_zero`, `sum_unitVec_mul_slice`, `zero_mul`, `cast_type`, `drop_drop`, `drop_take`, `take_take`	26
Total	52

Holor

Definitions

Name	Category	Theorems
`CPRankMax` 📖	CompData	3 math math: `cprankMax_upper_bound`, `cprankMax_1`, `cprankMax_nil`
`CPRankMax1` 📖	CompData	—
`assocLeft` 📖	CompOp	1 math math: `mul_assoc0`
`assocRight` 📖	CompOp	—
`cprank` 📖	CompOp	1 math math: `cprank_upper_bound`
`instAdd` 📖	CompOp	4 math math: `slice_add`, `cprankMax_add`, `mul_right_distrib`, `mul_left_distrib`
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	3 math math: `slice_sum`, `cprankMax_sum`, `sum_unitVec_mul_slice`
`instAddCommSemigroup` 📖	CompOp	—
`instAddGroup` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	—
`instAddSemigroup` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instModule` 📖	CompOp	—
`instNeg` 📖	CompOp	—
`instSMulOfMul` 📖	CompOp	1 math math: `mul_scalar_mul`
`instZero` 📖	CompOp	4 math math: `zero_mul`, `slice_zero`, `slice_unitVec_mul`, `mul_zero`
`mul` 📖	CompOp	10 math math: `mul_scalar_mul`, `zero_mul`, `mul_assoc`, `slice_unitVec_mul`, `mul_zero`, `mul_assoc0`, `mul_right_distrib`, `mul_left_distrib`, `cprankMax_mul`, `sum_unitVec_mul_slice`
`slice` 📖	CompOp	5 math math: `slice_sum`, `slice_zero`, `slice_unitVec_mul`, `slice_add`, `sum_unitVec_mul_slice`
`unitVec` 📖	CompOp	2 math math: `slice_unitVec_mul`, `sum_unitVec_mul_slice`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_type` 📖	mathematical	—	`Holor` `HolorIndex`	—	—
`cprankMax_1` 📖	mathematical	`CPRankMax1`	`CPRankMax`	—	`add_zero` `zero_add`
`cprankMax_add` 📖	mathematical	`CPRankMax`	`Holor` `instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`zero_add` `add_comm` `add_left_comm` `add_assoc`
`cprankMax_mul` 📖	mathematical	`CPRankMax` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`mul`	—	`mul_zero` `mul_left_distrib` `cprankMax_add` `cprankMax_1`
`cprankMax_nil` 📖	mathematical	—	`CPRankMax`	—	`zero_add` `add_zero`
`cprankMax_sum` 📖	mathematical	`CPRankMax` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`Finset.card` `Finset.sum` `Holor` `instAddCommMonoid`	—	`Finset.induction_on` `instIsEmptyFalse` `Finset.card_insert_of_notMem` `Finset.sum_insert` `cprankMax_add` `Finset.mem_insert_self`
`cprankMax_upper_bound` 📖	mathematical	—	`CPRankMax` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instOne`	—	`cprankMax_nil` `cprankMax_mul` `Finset.card_range` `cprankMax_sum` `Finset.card_attach` `Finset.mem_range` `Subtype.prop` `sum_unitVec_mul_slice`
`cprank_upper_bound` 📖	mathematical	—	`cprank` `Nat.instOne`	—	`Nat.find_min'` `cprankMax_upper_bound`
`holor_index_cons_decomp` 📖	—	—	—	—	`List.forall₂_nil_left_iff`
`mul_assoc` 📖	mathematical	—	`Holor` `mul` `Semigroup.toMul`	—	`mul_assoc0`
`mul_assoc0` 📖	mathematical	—	`mul` `Semigroup.toMul` `assocLeft`	—	`assocLeft.eq_1` `mul_assoc` `HolorIndex.take_take` `HolorIndex.drop_take` `HolorIndex.drop_drop` `cast_type`
`mul_left_distrib` 📖	mathematical	—	`mul` `Distrib.toMul` `Holor` `instAdd` `Distrib.toAdd`	—	`left_distrib` `Distrib.leftDistribClass`
`mul_right_distrib` 📖	mathematical	—	`mul` `Distrib.toMul` `Holor` `instAdd` `Distrib.toAdd`	—	`add_mul` `Distrib.rightDistribClass`
`mul_scalar_mul` 📖	mathematical	—	`mul` `Holor` `instSMulOfMul`	—	`Subtype.coe_eta`
`mul_zero` 📖	mathematical	—	`mul` `MulZeroClass.toMul` `Holor` `instZero` `MulZeroClass.toZero`	—	`MulZeroClass.mul_zero`
`slice_add` 📖	mathematical	—	`Holor` `instAdd` `slice`	—	—
`slice_eq` 📖	—	`slice`	—	—	`holor_index_cons_decomp`
`slice_sum` 📖	mathematical	—	`Finset.sum` `Holor` `instAddCommMonoid` `slice`	—	`Finset.induction_on` `Finset.sum_insert` `slice_add`
`slice_unitVec_mul` 📖	mathematical	—	`slice` `mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `unitVec` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Holor` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`zero_add` `Subtype.coe_eta` `one_mul` `MulZeroClass.zero_mul`
`slice_zero` 📖	mathematical	—	`slice` `Holor` `instZero`	—	—
`sum_unitVec_mul_slice` 📖	mathematical	—	`Finset.sum` `Finset` `Finset.instMembership` `Finset.range` `Holor` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.attach` `mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `unitVec` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `slice` `Finset.mem_range` `Subtype.prop`	—	`slice_eq` `Finset.mem_range` `Subtype.prop` `slice_sum` `Finset.sum_congr` `slice_unitVec_mul` `Finset.sum_eq_single` `Finset.mem_attach`
`zero_mul` 📖	mathematical	—	`mul` `MulZeroClass.toMul` `Holor` `instZero` `MulZeroClass.toZero`	—	`MulZeroClass.zero_mul`

HolorIndex

Definitions

Name	Category	Theorems
`assocLeft` 📖	CompOp	—
`assocRight` 📖	CompOp	3 math math: `drop_take`, `take_take`, `drop_drop`
`drop` 📖	CompOp	2 math math: `drop_take`, `drop_drop`
`take` 📖	CompOp	2 math math: `drop_take`, `take_take`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_type` 📖	mathematical	—	`HolorIndex`	—	—
`drop_drop` 📖	mathematical	—	`drop` `assocRight`	—	`cast_type`
`drop_take` 📖	mathematical	—	`take` `drop` `assocRight`	—	`cast_type`
`take_take` 📖	mathematical	—	`take` `assocRight`	—	`cast_type` `inf_of_le_left`

(root)

Definitions

Name	Category	Theorems
`Holor` 📖	CompOp	14 math math: `Holor.mul_scalar_mul`, `Holor.zero_mul`, `Holor.slice_sum`, `Holor.mul_assoc`, `Holor.slice_zero`, `Holor.slice_unitVec_mul`, `Holor.slice_add`, `Holor.mul_zero`, `Holor.cprankMax_add`, `Holor.cprankMax_sum`, `Holor.cast_type`, `Holor.mul_right_distrib`, `Holor.mul_left_distrib`, `Holor.sum_unitVec_mul_slice`
`HolorIndex` 📖	CompOp	2 math math: `HolorIndex.cast_type`, `Holor.cast_type`

---

← Back to Index