Skip to content

Commit f35bace

Browse files
committed
Add WeakSpace to Mathlib.lean
1 parent f785f4f commit f35bace

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2097,6 +2097,7 @@ public import Mathlib.Analysis.Normed.Module.Shrink
20972097
public import Mathlib.Analysis.Normed.Module.Span
20982098
public import Mathlib.Analysis.Normed.Module.TransferInstance
20992099
public import Mathlib.Analysis.Normed.Module.WeakDual
2100+
public import Mathlib.Analysis.Normed.Module.WeakSpace
21002101
public import Mathlib.Analysis.Normed.MulAction
21012102
public import Mathlib.Analysis.Normed.Operator.Asymptotics
21022103
public import Mathlib.Analysis.Normed.Operator.Banach

0 commit comments

Comments
 (0)