Theorem Equiv.coe_embeddingFinSucc_symm

Modification history

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.coe_embeddingFinSucc_symmView on Github →