Mathlib Changelog
v4
Changelog
About
Github
Def
Equiv.Set.prod_singleton_right
Modification history
2024-01-29 06:37
Mathlib/Data/Set/Prod.lean
feat(Algebra/InfiniteSum): drop `[T2Space _]` assumption (#10060) …
Deleted
Equiv.Set.prod_singleton_right
View on Github →
2024-01-27 17:46
Mathlib/Data/Set/Prod.lean
feat(Topology/Algebra/InfiniteSum/Basic): add some lemmas on `tsum`s (#10038) …
Added
Equiv.Set.prod_singleton_right
View on Github →