diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean index cb97ca40d8..4ff5416ccb 100644 --- a/library/data/nat/bigops.lean +++ b/library/data/nat/bigops.lean @@ -192,8 +192,4 @@ proposition prod_range_offset (m n : ℕ) (f : ℕ → A) : end set - - - - end nat