Skip to content

Commit 5521248

Browse files
faenuccioParcly-Taxelkim-em
committed
feat: port Analysis.NormedSpace.LinearIsometry (#3289)
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent 06aa02b commit 5521248

File tree

2 files changed

+1218
-0
lines changed

2 files changed

+1218
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -373,6 +373,7 @@ import Mathlib.Analysis.NormedSpace.ContinuousLinearMap
373373
import Mathlib.Analysis.NormedSpace.Extr
374374
import Mathlib.Analysis.NormedSpace.IndicatorFunction
375375
import Mathlib.Analysis.NormedSpace.Int
376+
import Mathlib.Analysis.NormedSpace.LinearIsometry
376377
import Mathlib.Analysis.NormedSpace.MStructure
377378
import Mathlib.Analysis.NormedSpace.Pointwise
378379
import Mathlib.Analysis.NormedSpace.Ray

0 commit comments

Comments
 (0)