Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.noncomm_prod_union_of_disjoint

Modification history

2021-07-08 14:46

src/data/finset/noncomm_prod.lean

feat(data/finset/noncomm_prod): noncomm_prod_union_of_disjoint (#8169)

Added finset.noncomm_prod_union_of_disjoint View on Github →