| Metric | Count |
|---|
DefinitionsFiniteDimensionalOrder, InfiniteDimensionalOrder, comap, injStrictMono, instFintypeOfDecidableLT, longestOf, map, mk, range, withLength, RelSeries, append, cons, drop, eraseLast, fromListChain', fromListIsChain, head, inductionOn, inductionOn', insertNth, instCoeFunForallFinHAddNatLengthOfNat, instInhabited, last, length, longestOf, map, membership, ofLE, reverse, singleton, smash, snoc, tail, take, toFun, toList, withLength, InfiniteDimensional | 39 |
TheoremsofUnique, apply_add_index_le_apply_add_index_int, apply_add_index_le_apply_add_index_nat, comap_length, comap_toFun, exists_relSeries_covBy, exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot, head_add_length_le_int, head_add_length_le_nat, head_le, head_le_last, head_map, head_range, last_map, last_range, length_lt_card, length_range, length_withLength, longestOf_is_longest, longestOf_len_unique, map_length, map_toFun, mk_length, mk_toFun, monotone, nonempty_of_finiteDimensionalOrder, nonempty_of_infiniteDimensionalOrder, range_apply, strictMono, append_apply_left, append_apply_right, append_assoc, append_cons, append_length, append_singleton_left, append_toFun, apply_last, apply_zero, coe_ofLE, cons_cast_succ, cons_length, cons_self_tail, drop_length, eraseLast_last_rel_last, eraseLast_length, eraseLast_toFun, ext, fromListChain'_cons, fromListIsChain_cons, fromListIsChain_length, fromListIsChain_toFun, getLast_toList, head_append, head_cons, head_drop, head_eraseLast, head_fromListChain', head_fromListIsChain, head_map, head_mem, head_reverse, head_singleton, head_smash, head_snoc, head_tail, head_take, head_toList, insertNth_length, insertNth_toFun, instIsEmpty, instNonempty, isChain_toList, last_append, last_cons, last_drop, last_eraseLast, last_map, last_mem, last_reverse, last_singleton, last_smash, last_snoc, last_snoc', last_tail, last_take, length_eq_zero, length_le_length_longestOf, length_ne_zero, length_ne_zero_of_nontrivial, length_pos, length_pos_of_nontrivial, length_toList, length_withLength, map_apply, map_length, mem_def, mem_snoc, mem_toList, nonempty_of_finiteDimensional, nonempty_of_infiniteDimensional, ofLE_length, ofLE_toFun, rel_of_lt, rel_or_eq_of_le, reverse_apply, reverse_length, reverse_reverse, singleton_length, singleton_toFun, smash_castAdd, smash_castLE, smash_length, smash_natAdd, smash_succ_castAdd, smash_succ_natAdd, snoc_castSucc, snoc_cast_castSucc, snoc_length, snoc_self_eraseLast, step, subsingleton_of_length_eq_zero, tail_cons, tail_length, tail_toFun, take_length, toList_append, toList_chain', toList_cons, toList_eraseLast, toList_fromListChain', toList_fromListIsChain, toList_getElem, toList_getElem_eq_apply, toList_getElem_eq_apply_of_lt_length, toList_getElem_zero_eq_head, toList_injective, toList_ne_nil, toList_singleton, toList_snoc, toList_tail, exists_longest_relSeries, inv, exists_relSeries_with_length, inv, inv_of_finiteDimensional, of_finiteDimensional, finiteDimensional_iff, finiteDimensional_inv, finiteDimensional_or_infiniteDimensional, infiniteDimensional_iff, infiniteDimensional_inv, not_finiteDimensional_iff, not_infiniteDimensional_iff, finiteDimensionalOrder_or_infiniteDimensionalOrder, infiniteDimensionalOrder_of_strictMono, not_finiteDimensionalOrder_iff, not_infiniteDimensionalOrder_iff | 157 |
| Total | 196 |
| Name | Category | Theorems |
|---|
append 📖 | CompOp | 10 mathmath: append_singleton_left, append_cons, last_append, append_length, append_assoc, append_apply_right, toList_append, head_append, append_apply_left, append_toFun
|
cons 📖 | CompOp | 11 mathmath: tail_cons, append_singleton_left, append_cons, last_cons, head_cons, cons_self_tail, cons_cast_succ, cons_length, toList_cons, fromListChain'_cons, fromListIsChain_cons
|
drop 📖 | CompOp | 3 mathmath: last_drop, head_drop, drop_length
|
eraseLast 📖 | CompOp | 12 mathmath: CompositionSeries.last_eraseLast_le, head_eraseLast, eraseLast_toFun, last_eraseLast, eraseLast_length, CompositionSeries.mem_eraseLast, toList_eraseLast, eraseLast_last_rel_last, CompositionSeries.mem_eraseLast_of_ne_of_mem, CompositionSeries.eq_snoc_eraseLast, CompositionSeries.isMaximal_eraseLast_last, snoc_self_eraseLast
|
fromListChain' 📖 | CompOp | — |
fromListIsChain 📖 | CompOp | 8 mathmath: head_fromListChain', fromListIsChain_toFun, fromListIsChain_length, head_fromListIsChain, toList_fromListIsChain, toList_fromListChain', fromListChain'_cons, fromListIsChain_cons
|
head 📖 | CompOp | 35 mathmath: LTSeries.head_add_length_le_nat, head_snoc, LTSeries.head_le_last, LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot, isFiniteLength_iff_exists_compositionSeries, head_fromListChain', head_singleton, LTSeries.head_range, head_eraseLast, head_toList, LTSeries.head_map, IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime, apply_zero, exists_compositionSeries_of_isNoetherian_isArtinian, Order.coheight_eq_iSup_head_eq, PrimeSpectrum.exist_ltSeries_mem_one_of_mem_last, head_reverse, cons_self_tail, Order.exists_series_of_coheight_eq_coe, Order.coheight_eq_top_iff, CompositionSeries.head_le_of_mem, Order.exists_series_of_le_coheight, last_reverse, LTSeries.head_add_length_le_int, toList_getElem_zero_eq_head, head_mem, head_take, head_fromListIsChain, head_map, LTSeries.head_le, head_drop, Order.coheight_eq, head_tail, CompositionSeries.head_le, Order.length_le_coheight_head
|
inductionOn 📖 | CompOp | — |
inductionOn' 📖 | CompOp | — |
insertNth 📖 | CompOp | 2 mathmath: insertNth_length, insertNth_toFun
|
instCoeFunForallFinHAddNatLengthOfNat 📖 | CompOp | — |
instInhabited 📖 | CompOp | — |
last 📖 | CompOp | 38 mathmath: LTSeries.head_add_length_le_nat, CompositionSeries.le_last, CompositionSeries.last_eraseLast_le, LTSeries.head_le_last, LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot, Order.exists_series_of_le_height, last_mem, isFiniteLength_iff_exists_compositionSeries, CompositionSeries.lt_last_of_mem_eraseLast, Ideal.exists_ltSeries_length_eq_height, last_cons, IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime, exists_compositionSeries_of_isNoetherian_isArtinian, last_take, head_reverse, getLast_toList, last_eraseLast, LTSeries.last_map, Ideal.exists_ltSeries_of_hasGoingDown, last_tail, LTSeries.last_range, last_reverse, LTSeries.head_add_length_le_int, Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support, Order.exists_series_of_height_eq_coe, apply_last, last_map, last_drop, eraseLast_last_rel_last, CompositionSeries.eq_snoc_eraseLast, LTSeries.height_last_longestOf, CompositionSeries.isMaximal_eraseLast_last, CompositionSeries.le_last_of_mem, last_singleton, Order.height_eq_iSup_last_eq, Order.length_le_height_last, Order.height_eq_top_iff, snoc_self_eraseLast
|
length 📖 | CompOp | 94 mathmath: LTSeries.head_add_length_le_nat, Module.length_compositionSeries, Order.LTSeries.length_le_krullDim, Order.krullDim_lt_coe_iff, smash_succ_castAdd, Order.length_le_coheight, LTSeries.map_length, LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot, Order.exists_series_of_le_height, Order.le_krullDim_iff, tail_toFun, Ideal.exists_ltSeries_length_eq_height, LTSeries.length_withLength, CompositionSeries.lt_succ, ofLE_length, length_pos, take_length, Order.krullDim_eq_iSup_length, smash_castLE, apply_zero, eraseLast_toFun, length_pos_of_nontrivial, Order.coheight_eq_iSup_head_eq, PrimeSpectrum.exist_ltSeries_mem_one_of_mem_last, snoc_cast_castSucc, cons_self_tail, snoc_length, length_withLength, LTSeries.strictMono, tail_length, Order.exists_series_of_coheight_eq_coe, smash_castAdd, fromListIsChain_length, last_eraseLast, map_length, Order.length_le_height, CompositionSeries.exists_last_eq_snoc_equivalent, cons_cast_succ, Ideal.exists_ltSeries_of_hasGoingDown, append_length, cons_length, Order.coheight_eq_top_iff, singleton_length, CompositionSeries.Equivalent.length_eq, CompositionSeries.strictMono, smash_succ_natAdd, append_apply_right, SetRel.FiniteDimensional.exists_longest_relSeries, Order.coheight_le_iff', Order.exists_series_of_le_coheight, SetRel.finiteDimensional_iff, CompositionSeries.injective, LTSeries.length_lt_card, eraseLast_length, LTSeries.head_add_length_le_int, LTSeries.longestOf_is_longest, snoc_castSucc, reverse_length, reverse_apply, mem_def, LTSeries.exists_relSeries_covBy, Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support, append_apply_left, Order.exists_series_of_height_eq_coe, LTSeries.length_range, apply_last, LTSeries.mk_length, length_le_length_longestOf, toList_getElem, length_eq_zero, Order.height_le_iff, Order.krullDim_eq_length_of_finiteDimensionalOrder, SetRel.InfiniteDimensional.exists_relSeries_with_length, Order.height_le_iff', last_snoc', step, smash_natAdd, smash_length, toList_getElem_eq_apply, Order.index_le_height, Order.coheight_eq, Order.rev_index_le_coheight, head_tail, SetRel.infiniteDimensional_iff, Order.height_eq_iSup_last_eq, drop_length, Order.length_le_height_last, length_toList, Order.height_eq_top_iff, Order.length_le_coheight_head, append_toFun, LTSeries.comap_length, Order.coheight_le_iff, LTSeries.monotone
|
longestOf 📖 | CompOp | 1 mathmath: length_le_length_longestOf
|
map 📖 | CompOp | 4 mathmath: map_length, last_map, head_map, map_apply
|
membership 📖 | CompOp | 11 mathmath: last_mem, mem_toList, length_ne_zero, length_pos, CompositionSeries.ext_iff, mem_def, CompositionSeries.mem_eraseLast, head_mem, subsingleton_of_length_eq_zero, length_eq_zero, mem_snoc
|
ofLE 📖 | CompOp | 3 mathmath: ofLE_toFun, ofLE_length, coe_ofLE
|
reverse 📖 | CompOp | 5 mathmath: head_reverse, reverse_reverse, last_reverse, reverse_length, reverse_apply
|
singleton 📖 | CompOp | 6 mathmath: toList_singleton, head_singleton, append_singleton_left, singleton_toFun, singleton_length, last_singleton
|
smash 📖 | CompOp | 9 mathmath: smash_succ_castAdd, smash_castLE, head_smash, smash_castAdd, smash_succ_natAdd, smash_natAdd, smash_length, CompositionSeries.Equivalent.smash, last_smash
|
snoc 📖 | CompOp | 13 mathmath: head_snoc, last_snoc, snoc_cast_castSucc, snoc_length, CompositionSeries.exists_last_eq_snoc_equivalent, CompositionSeries.Equivalent.snoc, CompositionSeries.snoc_eraseLast_last, snoc_castSucc, CompositionSeries.eq_snoc_eraseLast, last_snoc', toList_snoc, snoc_self_eraseLast, mem_snoc
|
tail 📖 | CompOp | 7 mathmath: tail_cons, tail_toFun, cons_self_tail, tail_length, last_tail, head_tail, toList_tail
|
take 📖 | CompOp | 3 mathmath: take_length, last_take, head_take
|
toFun 📖 | CompOp | 55 mathmath: CompositionSeries.le_last, smash_succ_castAdd, rel_or_eq_of_le, LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot, tail_toFun, ofLE_toFun, CompositionSeries.lt_succ, LTSeries.range_apply, smash_castLE, apply_zero, coe_ofLE, fromListIsChain_toFun, last_take, eraseLast_toFun, PrimeSpectrum.exist_ltSeries_mem_one_of_mem_last, snoc_cast_castSucc, LTSeries.strictMono, smash_castAdd, last_eraseLast, LTSeries.comap_toFun, cons_cast_succ, LTSeries.map_toFun, singleton_toFun, LTSeries.apply_add_index_le_apply_add_index_nat, CompositionSeries.strictMono, smash_succ_natAdd, append_apply_right, Order.coheight_eq_index_of_length_eq_head_coheight, CompositionSeries.injective, snoc_castSucc, reverse_apply, mem_def, LTSeries.exists_relSeries_covBy, append_apply_left, apply_last, toList_getElem, rel_of_lt, map_apply, last_snoc', LTSeries.mk_toFun, step, smash_natAdd, LTSeries.head_le, toList_getElem_eq_apply, Order.index_le_height, head_drop, Order.rev_index_le_coheight, CompositionSeries.inj, head_tail, CompositionSeries.head_le, append_toFun, LTSeries.monotone, LTSeries.apply_add_index_le_apply_add_index_int, Order.height_eq_index_of_length_eq_height_last, toList_getElem_eq_apply_of_lt_length
|
toList 📖 | CompOp | 21 mathmath: toList_singleton, mem_toList, head_toList, getLast_toList, Ideal.exists_ltSeries_of_hasGoingDown, toList_getElem_zero_eq_head, toList_append, toList_injective, toList_chain', toList_eraseLast, CompositionSeries.toList_sorted, toList_cons, toList_fromListIsChain, toList_fromListChain', toList_getElem_eq_apply, CompositionSeries.toList_nodup, toList_tail, toList_snoc, length_toList, isChain_toList, toList_getElem_eq_apply_of_lt_length
|
withLength 📖 | CompOp | 1 mathmath: length_withLength
|