Theorem List.prod_one_cons

Modification history

2025-11-16 12:52
Mathlib/Algebra/BigOperators/Group/List/Defs.lean
chore: adaptations for batteries#1486 (#31182) …
Deleted List.prod_one_consView on Github →
2025-01-10 04:57
Mathlib/Algebra/BigOperators/Group/List/Basic.lean
chore: split Algebra/BigOperators/Group/List (#20625)
Modified List.prod_one_consView on Github →
2024-03-25 20:19
Mathlib/Data/List/BigOperators/Basic.lean
feat: add lemma List.prod_map_one (#11112) …
Added List.prod_one_consView on Github →