Commit 2025-05-16 03:37 9e1731c2

View on Github →

feat(Data/Fin/Tuple/Embedding): create embeddings of Fin Nat to types (#24167) Define

Fin.Embedding.cons, Fin.Embedding.tail
Fin.Embedding.snoc, Fin.Embedding.init
Fin.Embedding.append analogously to Fin.cons, Fin.snoc, Fin.append.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fin/Tuple/Basic.lean

added theorem Fin.append_comp_sumElim

added theorem Fin.append_injective_iff

added theorem Fin.snoc_injective_iff

added theorem Fin.snoc_injective_of_injective

Created Mathlib/Data/Fin/Tuple/Embedding.lean

added def Fin.Embedding.append

added theorem Fin.Embedding.coe_append

added theorem Fin.Embedding.coe_cons

added theorem Fin.Embedding.coe_snoc

added theorem Fin.Embedding.coe_tail

added def Fin.Embedding.cons

added def Fin.Embedding.init

added theorem Fin.Embedding.init_snoc

added def Fin.Embedding.snoc

added theorem Fin.Embedding.snoc_castSucc

added theorem Fin.Embedding.snoc_last

added def Fin.Embedding.tail

added theorem Fin.Embedding.tail_cons

Modified Mathlib/Data/Set/Disjoint.lean

added theorem Set.disjoint_range_iff

Modified Mathlib/Data/Sum/Basic.lean

modified theorem Function.Injective.sumElim

modified theorem Sum.elim_injective

Modified Mathlib/Order/Fin/Basic.lean

added theorem Fin.natAdd_injective