Theorem Finset.noncommProd_mulSingle

Modification history

2025-11-28 16:39
Mathlib/Data/Finset/NoncommProd.lean
chore(to_additive): remove redundant entries from `abbreviationDict` (#32092) …
Added Finset.noncommProd_mulSingleView on Github →