Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-09 12:25 e00bfc1e

View on Github →

feat(data/fin/tuple/basic): injectivity of fin.cons x xs (#17779)

Estimated changes

Modified src/data/fin/tuple/basic.lean

added def fin.cons_cases

added theorem fin.cons_cases_cons

modified def fin.cons_induction

deleted theorem fin.cons_induction_cons

added theorem fin.cons_injective_iff

added theorem fin.cons_injective_of_injective

Modified src/data/fin/tuple/nat_antidiagonal.lean

Modified src/data/list/range.lean

modified theorem list.nodup_of_fn

added theorem list.nodup_of_fn_of_injective