Skip to content

Commit 5bb521a

Browse files
committed
fix(Combinatorics/Enumerative/Bonferroni): make "Bonferroni.lean" a module
1 parent ae51ff5 commit 5bb521a

1 file changed

Lines changed: 5 additions & 1 deletion

File tree

Mathlib/Combinatorics/Enumerative/Bonferroni.lean

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,9 @@ Copyright (c) 2026 Louis (Yiyang) Liu. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Louis (Yiyang) Liu
55
-/
6-
import Mathlib.Data.Nat.Choose.Sum
6+
module
7+
8+
public import Mathlib.Data.Nat.Choose.Sum
79

810
/-!
911
# Bonferroni inequalities
@@ -23,6 +25,8 @@ by truncating the inclusion–exclusion formula for a finite union of sets.
2325
the cardinality of the union.
2426
-/
2527

28+
@[expose] public section
29+
2630
open Nat Int Set
2731

2832
/-! ### Binomial identities -/

0 commit comments

Comments
 (0)