Theorem Fin.coe_succAboveEmb

Modification history

2024-05-30 11:57

Mathlib/Data/Fin/Basic.lean

chore: Delete `Data.Fin.OrderHom` (#13147) …

Modified Fin.coe_succAboveEmb View on Github →

2024-05-30 05:34

Mathlib/Data/Fin/OrderHom.lean

refactor: split Fin.succAboveEmb into an Embedding and an OrderEmbedding (#13341)

Added Fin.coe_succAboveEmb View on Github →