Commit 2024-03-25 20:19 2d2e953b

View on Github →

feat: add lemma List.prod_map_one (#11112) Adds the lemma, and to_additive tags it

Estimated changes

Modified Mathlib/Data/List/BigOperators/Basic.lean

added theorem List.prod_map_one

added theorem List.prod_one_cons