chore(algebra/big_operators/finprod): remove outdated todo (#9900)

leanprover-community · Oct 23, 2021 · a58ae54 · a58ae54
1 parent bd81d55
commit a58ae54
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/src/algebra/big_operators/finprod.lean b/src/algebra/big_operators/finprod.lean
@@ -61,11 +61,7 @@ The first arguments in all definitions and lemmas is the codomain of the functio
 operator. This is necessary for the heuristic in `@[to_additive]`.
 See the documentation of `to_additive.attr` for more information.
 
-## Todo
-
 We did not add `is_finite (X : Type) : Prop`, because it is simply `nonempty (fintype X)`.
-There is work on `fincard` in the pipeline, which returns the cardinality of `X` if it
-is finite, and 0 otherwise.
 
 ## Tags