diff --git a/LeanBridge.lean b/LeanBridge.lean
index 9009ac5d..362f9558 100644
--- a/LeanBridge.lean
+++ b/LeanBridge.lean
@@ -1 +1,2 @@
 import LeanBridge.Example
+import LeanBridge.Galois
diff --git a/LeanBridge/Galois.lean b/LeanBridge/Galois.lean
new file mode 100644
index 00000000..a91acead
--- /dev/null
+++ b/LeanBridge/Galois.lean
@@ -0,0 +1,33 @@
+import IdealArithmetic.Galois.Examples.DegSixA4C2
+
+/-!
+# Galois-group certificates (bridged from `CertifyingInvariantsNF`)
+
+This module makes the Galois-group certification library
+(`IdealArithmetic.Galois`, developed in the `CertifyingInvariantsNF` project)
+available inside LeanBridge, linking LMFDB Galois-group data (`nTk` labels) to
+formal Lean proofs.
+
+The showcase result, re-exported below: the degree-6 number field
+`ℚ[x]/(x⁶ − 5x⁴ − 50x² + 125)` has Galois group `A₄ × C₂` — the transitive
+group `6T6`, of order `24`. The underlying library also provides reusable
+machinery (Dedekind/Frobenius cycle-type certificates, the discriminant square
+test, cubic Galois-group determination) not re-exported here.
+-/
+
+namespace LeanBridge.Galois
+
+open Polynomial IdealArithmetic.Galois.DegSix
+
+/-- **`6T6`.** The Galois group of `x⁶ − 5x⁴ − 50x² + 125` over `ℚ` is isomorphic
+to `A₄ × C₂`. Bridged from `IdealArithmetic.Galois.DegSix`. -/
+theorem galoisGroup_degSix_isA4timesC2 :
+    Nonempty ((f.map (Int.castRingHom ℚ)).Gal ≃*
+      alternatingGroup (Fin 4) × Multiplicative (ZMod 2)) :=
+  gal_f_mulEquiv
+
+/-- The Galois group of that degree-6 field has order `24`. -/
+theorem galoisGroup_degSix_card : Nat.card (f.map (Int.castRingHom ℚ)).Gal = 24 :=
+  card_gal_f
+
+end LeanBridge.Galois
diff --git a/lake-manifest.json b/lake-manifest.json
index 9eb86468..60cc40e7 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,7 +1,17 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/mathlib4.git",
+ [{"url": "https://github.com/CBirkbeck/CertifyingInvariantsNF.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "11b4888b5523b30ec0c8cb8c18a0fd5469524f2a",
+   "name": "IdealArithmetic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "galois-v431-bump",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
diff --git a/lakefile.toml b/lakefile.toml
index de33880b..a23f2e52 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -20,5 +20,10 @@ name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
 rev = "v4.31.0"
 
+[[require]]
+name = "IdealArithmetic"
+git = "https://github.com/CBirkbeck/CertifyingInvariantsNF.git"
+rev = "galois-v431-bump"
+
 [[lean_lib]]
 name = "LeanBridge"