Commit 2026-03-11 02:31 218bca71

View on Github →

feat(Data/Finsupp/Order): {map,emb}Domain preserve tsub (#36369) mapDomain by an injective map, and embDomain, preserve truncated subtraction.

Estimated changes

added theorem Finsupp.embDomain_tsub
added theorem Finsupp.mapDomain_tsub