chore(data/list/prod): remove an out of date comment (#11058)

Due to changes in the library structure this comment is no longer relevant.
leanprover-community · Dec 26, 2021 · 34e79d6 · 34e79d6
1 parent 266d12b
commit 34e79d6
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/src/data/list/prod_monoid.lean b/src/data/list/prod_monoid.lean
@@ -9,8 +9,6 @@ import data.list.big_operators
 # Products / sums of lists of terms of a monoid
 
 This file provides basic results about `list.prod` (definition in `data.list.defs`) in a monoid.
-It is in a separate file so that `data.list.big_operators` does not depend on
-`algebra.group_power.basic`.
 -/
 
 open nat