Theorem List.prod_induction

Modification history

2025-01-10 04:57

Mathlib/Algebra/BigOperators/Group/List/Basic.lean

chore: split Algebra/BigOperators/Group/List (#20625)

Modified List.prod_induction View on Github →

2023-11-03 16:55

Mathlib/Data/List/BigOperators/Basic.lean

feat: expand `Finset.noncommProd` API (#8155)

Added List.prod_induction View on Github →