Skip to content

Commit c285cf7

Browse files
urkudParcly-Taxel
andcommitted
feat: port Analysis.InnerProductSpace.TwoDim (#4602)
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
1 parent 802488e commit c285cf7

File tree

2 files changed

+678
-0
lines changed

2 files changed

+678
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -586,6 +586,7 @@ import Mathlib.Analysis.InnerProductSpace.PiL2
586586
import Mathlib.Analysis.InnerProductSpace.Positive
587587
import Mathlib.Analysis.InnerProductSpace.Projection
588588
import Mathlib.Analysis.InnerProductSpace.Symmetric
589+
import Mathlib.Analysis.InnerProductSpace.TwoDim
589590
import Mathlib.Analysis.InnerProductSpace.l2Space
590591
import Mathlib.Analysis.LocallyConvex.AbsConvex
591592
import Mathlib.Analysis.LocallyConvex.BalancedCoreHull

0 commit comments

Comments
 (0)