Theorem List.Perm.prod_eq

Modification history

2024-10-14 08:17
Mathlib/Algebra/BigOperators/Group/List.lean
chore: use foldr in List.prod (#17223) …
Modified List.Perm.prod_eqView on Github →
2024-09-30 13:03
Mathlib/Algebra/BigOperators/Group/List.lean
feat: add missing List.foldr lemmas (#17222)
Modified List.Perm.prod_eqView on Github →
2024-04-06 10:45
Mathlib/Algebra/BigOperators/List/Basic.lean
chore(Data/List): Do not depend on algebra (#11845) …
Modified List.Perm.prod_eqView on Github →
2023-01-11 16:31
Mathlib/Data/List/Perm.lean
feat: port Mathlib.Data.List.Perm (#1478)
Added List.Perm.prod_eqView on Github →