Mathlib Changelog
v4
Changelog
About
Github
Theorem
Equiv.embeddingFinSucc_snd
Modification history
2025-07-04 07:44
Mathlib/Logic/Equiv/Fin/Basic.lean
chore: further whitespace fixes (#26708) …
Modified
Equiv.embeddingFinSucc_snd
View 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_snd
View on Github →