Theorem Finsupp.mapDomain_tsub

Modification history

2026-03-11 02:31
Mathlib/Data/Finsupp/Order.lean
feat(Data/Finsupp/Order): `{map,emb}Domain` preserve tsub (#36369) …
Added Finsupp.mapDomain_tsubView on Github →