Theorem Fin.succ_injective

Modification history

2024-07-27 16:57
Mathlib/Data/Fin/Basic.lean
chore: qualify uses of ext and ext_iff lemmas (#15106) …
Modified Fin.succ_injectiveView on Github →
2024-05-23 11:18
Mathlib/Data/Fin/Basic.lean
chore: Remove order dependencies to `Data.Fin.Basic` (#13005) …
Modified Fin.succ_injectiveView on Github →
2024-02-01 16:22
Mathlib/Data/Fin/Basic.lean
feat(Data/Fin/Basic): Improvement and extension of order results (#10156) …
Modified Fin.succ_injectiveView on Github →
2023-01-12 19:47
Mathlib/Data/Fin/Basic.lean
feat: port Data.Fin.Basic (#1084) …
Added Fin.succ_injectiveView on Github →