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 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersFin.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.
Fin.induction_append_left
Plain-language statement
Fin.induction on m + n for i ≤ m steps is equivalent to Fin.induction on m for i steps.
Source project: ArkLib
Person-level attribution pending.
Fin.induction_append_right
Plain-language statement
Fin.induction on m + n for m + i steps is equivalent to Fin.induction on n on i steps on the result of Fin.induction on m.
Source project: ArkLib
Person-level attribution pending.