Skip to content

Commit b9cc405

Browse files
Parcly-Taxeleric-wieserADedeckerkim-em
committed
feat: port Topology.Algebra.Module.Multilinear (#3348)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: ADedecker <anatolededecker@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent 1a889c7 commit b9cc405

File tree

2 files changed

+599
-0
lines changed

2 files changed

+599
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1863,6 +1863,7 @@ import Mathlib.Topology.Algebra.InfiniteSum.Ring
18631863
import Mathlib.Topology.Algebra.Localization
18641864
import Mathlib.Topology.Algebra.Module.Basic
18651865
import Mathlib.Topology.Algebra.Module.LinearPMap
1866+
import Mathlib.Topology.Algebra.Module.Multilinear
18661867
import Mathlib.Topology.Algebra.Module.Simple
18671868
import Mathlib.Topology.Algebra.Module.StrongTopology
18681869
import Mathlib.Topology.Algebra.Module.WeakDual

0 commit comments

Comments
 (0)