Skip to content

Commit f594449

Browse files
committed
fix import
1 parent d65b49e commit f594449

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

  • Mathlib/SetTheory/Cardinal/Cofinality

Mathlib/SetTheory/Cardinal/Cofinality/Club.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Violeta Hernández Palacios
66
module
77

88
public import Mathlib.Order.DirSupClosed
9+
public import Mathlib.Order.IsNormal
910
public import Mathlib.SetTheory.Cardinal.Cofinality.Basic
1011

1112
/-!

0 commit comments

Comments
 (0)