feat: Nobeling's theorem (#6286)

Nobeling's theorem: the Z-module of locally constant maps from a profinite set to the integers is free.

-  [x] depends on: #6360 
-  [x] depends on: #6373 
-  [x] depends on: #6395 
-  [x] depends on: #6396  
-  [x] depends on: #6432
-  [x] depends on: #6520
-  [x] depends on: #6578
-  [x] depends on: #6589 
-  [x] depends on: #6722 
-  [x] depends on: #7829 
-  [x] depends on: #7895 
-  [x] depends on: #7896 
-  [x] depends on: #7897  
-  [x] depends on: #7899

Mathlib.lean

@@ -3383,6 +3383,7 @@ import Mathlib.Topology.Category.Profinite.Basic
 import Mathlib.Topology.Category.Profinite.CofilteredLimit
 import Mathlib.Topology.Category.Profinite.EffectiveEpi
 import Mathlib.Topology.Category.Profinite.Limits
+import Mathlib.Topology.Category.Profinite.Nobeling
 import Mathlib.Topology.Category.Profinite.Product
 import Mathlib.Topology.Category.Profinite.Projective
 import Mathlib.Topology.Category.Stonean.Adjunctions