Theorem Equiv.embeddingFinSucc_fst

Modification history

2025-07-04 07:44
Mathlib/Logic/Equiv/Fin/Basic.lean
chore: further whitespace fixes (#26708) …
Modified Equiv.embeddingFinSucc_fstView on Github →
2024-04-17 12:17
Mathlib/Logic/Equiv/Fin.lean
feat: Equivalence between embeddings of `Fin (n + 1)`, and embeddings of `Fin n` together with a value outside the range. (#12151)
Added Equiv.embeddingFinSucc_fstView on Github →