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.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.
Fin.take_drop_addCases'
Plain-language statement
The concatenation of the first m elements and the last n - m elements of a tuple is the same as the original tuple.
Source project: ArkLib
Person-level attribution pending.
Finset.card_filter_prod_self_eq
Plain-language statement
The diagonal of s × s has the same cardinality as s.
Source project: ArkLib
Person-level attribution pending.
Finset.card_pick_subset
Plain-language statement
The cardinality of picked subset is min s.card n.
Source project: ArkLib
Person-level attribution pending.
Finset.card_prod_self_eq
Plain-language statement
The diagonal of s × s (intersection form) has the same cardinality as s.
Source project: ArkLib
Person-level attribution pending.