Skip to content

Commit 2495d85

Browse files
vihdzpvihdzp
committed
private import
1 parent 1a8cfb3 commit 2495d85

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

‎Mathlib/RingTheory/HahnSeries/Cardinal.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,10 @@ Authors: Violeta Hernández Palacios
55
-/
66
module
77

8-
public import Mathlib.Algebra.Group.Pointwise.Set.Card
98
public import Mathlib.RingTheory.HahnSeries.Multiplication
109

10+
import Mathlib.Algebra.Group.Pointwise.Set.Card
11+
1112
/-!
1213
# Cardinality of Hahn series
1314

0 commit comments

Comments
 (0)
⚡