Def Equiv.Set.prod_singleton_left

Modification history

2024-01-29 06:37

Mathlib/Data/Set/Prod.lean

feat(Algebra/InfiniteSum): drop `[T2Space _]` assumption (#10060) …

Deleted Equiv.Set.prod_singleton_left 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_left View on Github →