Theorem List.prod_induction_nonempty

Modification history

2025-11-04 12:44
Mathlib/Algebra/BigOperators/Group/List/Defs.lean
feat: add List.le_prod_of_submultiplicative and friends (#31016)
Added List.prod_induction_nonemptyView on Github →