diff --git a/src/data/list/prod_monoid.lean b/src/data/list/prod_monoid.lean index 2a4a6a018148e..6e5da7765b1bb 100644 --- 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