Skip to content

Commit 56ebf4c

Browse files
ADedeckermcdoll
andcommitted
feat: port Analysis.LocallyConvex.WithSeminorms (#4170)
Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
1 parent 468469a commit 56ebf4c

File tree

3 files changed

+779
-3
lines changed

3 files changed

+779
-3
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -438,6 +438,7 @@ import Mathlib.Analysis.LocallyConvex.Bounded
438438
import Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
439439
import Mathlib.Analysis.LocallyConvex.Polar
440440
import Mathlib.Analysis.LocallyConvex.StrongTopology
441+
import Mathlib.Analysis.LocallyConvex.WithSeminorms
441442
import Mathlib.Analysis.Normed.Field.Basic
442443
import Mathlib.Analysis.Normed.Field.InfiniteSum
443444
import Mathlib.Analysis.Normed.Field.UnitBall

0 commit comments

Comments
 (0)