Theorem Finset.prod_of_isEmpty

Modification history

2025-07-05 03:31
Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
chore(Algebra/BigOperators): rename variables away from greek letters (#26521) …
Modified Finset.prod_of_isEmptyView on Github →
2025-01-13 05:50
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
chore: split `Algebra/BigOperators/Group/{Multiset,Finset}` (#20629) …
Modified Finset.prod_of_isEmptyView on Github →
2024-06-16 19:40
Mathlib/Algebra/BigOperators/Group/Finset.lean
chore: Golf `Finset.prod_ite_of_true` (#13726) …
Added Finset.prod_of_isEmptyView on Github →