Theorem Finset.prod_eq_prod_iff_single

Modification history

2026-01-19 18:13
Mathlib/Algebra/BigOperators/Group/Finset/Piecewise.lean
feat(RingTheory/HahnSeries): generalise `IsDomain` instance (#34147)
Added Finset.prod_eq_prod_iff_singleView on Github →