We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 3991179 commit b1d0372Copy full SHA for b1d0372
FLT/HIMExperiments/module_topology.lean
@@ -1,3 +1,9 @@
1
+/-
2
+Copyright (c) 2024 Kevin Buzzaed. All rights reserved.
3
+Released under Apache 2.0 license as described in the file LICENSE.
4
+Authors: Kevin Buzzard, Hannah Scholz, Ludwig Monnerjahn
5
+-/
6
+
7
import Mathlib.RingTheory.TensorProduct.Basic -- we need tensor products of rings at some point
8
import Mathlib.Topology.Algebra.Module.Basic -- and we need topological rings and modules
9
/-
0 commit comments