Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersFin.dappend_eq_addCases
Plain-language statement
dappend is equal to addCases. Marked as csimp to allow for switching to the addCases implementation during execution.
Source project: ArkLib
Person-level attribution pending.
Fin.drop_addCases_right
Plain-language statement
Dropping the first n + m elements of an addCases u v, where v is a n'-tuple and m ≤ n', is the same as dropping the first m elements of v.
Source project: ArkLib
Person-level attribution pending.
Fin.drop_append_left
Plain-language statement
Version of drop_addCases_left that specializes addCases to append.
Source project: ArkLib
Person-level attribution pending.
Fin.drop_append_right
Plain-language statement
Version of drop_addCases_right that specializes addCases to append.
Source project: ArkLib
Person-level attribution pending.
Fin.drop_update_of_ge
Plain-language statement
drop commutes with update for indices at or after the drop point.
Source project: ArkLib
Person-level attribution pending.
Fin.happend_heq_right
Plain-language statement
Access into a heterogeneous append on the right, by value: if m ≤ ↑j, then happend u v j is (heterogeneously) the (↑j - m)-th entry of v.
Source project: ArkLib
Person-level attribution pending.