Theorem tprod_prod_uncurry

Modification history

2025-04-13 16:12
Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
chore(tprod): move tprod lemmas to protected namespace (#23959) …
Deleted tprod_prod_uncurryView on Github →
2025-03-14 06:42
Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
chore: review of `erw` in `Topology/` (#22914)
Added tprod_prod_uncurryView on Github →