We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 92bf783 commit 743eb0cCopy full SHA for 743eb0c
Mathlib.lean
@@ -6073,6 +6073,7 @@ public import Mathlib.RingTheory.Finiteness.Bilinear
6073
public import Mathlib.RingTheory.Finiteness.Cardinality
6074
public import Mathlib.RingTheory.Finiteness.Cofinite
6075
public import Mathlib.RingTheory.Finiteness.Defs
6076
+public import Mathlib.RingTheory.Finiteness.Descent
6077
public import Mathlib.RingTheory.Finiteness.Finsupp
6078
public import Mathlib.RingTheory.Finiteness.Ideal
6079
public import Mathlib.RingTheory.Finiteness.Lattice
0 commit comments