Commit 2023-12-11 16:31 de48aea2

View on Github →

feat: s × t = univ ↔ s = univ ∧ t = univ (#8976) for sets and finsets From LeanCamCombi

Estimated changes

added theorem Finset.product_eq_univ
modified theorem Finset.univ_product_univ
added theorem Set.prod_eq_univ