Verification run

Run 1

ImperialCollegeLondon/FLT branch main triggered via poller

failed commit fa42521b0360 toolchain lean-v4-30-0 prover lean took 1h 13m · finished 6w ago

./.apodeixis/tools/lean-semantic-extract.sh failed with exit code 1 (toolchain lean-v4-30-0, command: elan run leanprover/lean4:v4.30.0 -- ./.apodeixis/tools/lean-semantic-extract.sh)

Open project

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

(no log excerpt)

Command runs

git_clone exit 0 duration 845 ms · created 6/1/2026, 9:13:08 PM

git clone --depth 1 --branch main --single-branch https://github.com/ImperialCollegeLondon/FLT.git /var/lib/apodeixis/repos/job-12-source

Cloning into '/var/lib/apodeixis/repos/job-12-source'...

git_checkout exit 0 duration 21 ms · created 6/1/2026, 9:13:08 PM

git checkout fa42521b0360498552efa3be5fbddcf41d190871

Note: switching to 'fa42521b0360498552efa3be5fbddcf41d190871'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at fa42521 chore: bump mathlib to deb4715, fix breaking changes (#991)

lake_cache exit 1 duration 52s · created 6/1/2026, 9:13:08 PM

lake exe cache get

info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git
info: checkdecls: checking out revision '3d425859e73fcfbef85b9638c2a91708ef4a22d4'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'deb47159e3857969498932c93c085cc6550e4e48'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'a456461b368b71d2accd95234832cd9c174b5437'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'c5d5b8fe6e5158def25cd28eb94e4141ad97c843'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '515cf9d0c00ece5e661f6de4326a53dedc1e8ea1'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'a84b3e2475d5c5ab979567b1ad8aea21b764bcf8'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '558915ae105bfd8074e22d597613d1961822adc2'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '32dc18cde3684679f3c003de608743b57498c56f'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '6b907cf12b2e445ccb7c24bc208ef04a1f39e84c'
✔ [2/24] Built Cache.Init (445ms)
✔ [3/24] Built Cache.Lean (498ms)
✔ [4/24] Built Cache.Init:c.o (92ms)
✔ [5/24] Built Cache.Lean:c.o (115ms)
✔ [13/24] Built Batteries.Data.String.Basic:c.o (125ms)
✔ [14/24] Built Batteries.Data.Array.Match:c.o (193ms)
✔ [15/24] Built Batteries.Data.String.Matcher:c.o (175ms)
✔ [16/24] Built Cache.IO (1.7s)
✖ [17/24] Building Cache.Hashing (427ms)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/packages/checkdecls/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/.lake/packages/mathlib/Cache/Hashing.lean -o /apx/source/.lake/packages/mathlib/.lake/build/lib/lean/Cache/Hashing.olean -i /apx/source/.lake/packages/mathlib/.lake/build/lib/lean/Cache/Hashing.ilean -c /apx/source/.lake/packages/mathlib/.lake/build/ir/Cache/Hashing.c --setup /apx/source/.lake/packages/mathlib/.lake/build/ir/Cache/Hashing.setup.json --json
error: Cache/Hashing.lean:7:0: leantar not found in Lean sysroot. This toolchain may predate nightly-2026-03-09.
error: Lean exited with code 1
✔ [23/24] Built Cache.IO:c.o (1.2s)
Some required targets logged failures:
- Cache.Hashing
error: build failed

lean_checker exit 0 duration 1h 0m · created 6/1/2026, 9:13:08 PM

lake build

hlib.CategoryTheory.Comma.StructuredArrow.Basic (14s)
✔ [3093/3136] Built Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (6.4s)
✔ [3094/3136] Built Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (1.8s)
✔ [3095/3136] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal (1.7s)
✔ [3096/3136] Built Mathlib.CategoryTheory.Monoidal.Skeleton (1.5s)
✔ [3097/3138] Built Mathlib.Algebra.Module.Injective (6.5s)
✔ [3098/3138] Built Mathlib.CategoryTheory.Limits.Creates (4.1s)
✔ [3099/3140] Built Mathlib.RingTheory.Flat.Basic (6.0s)
✔ [3100/3140] Built Mathlib.CategoryTheory.Limits.Shapes.Products (13s)
✔ [3101/3143] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (1.7s)
✔ [3102/3143] Built Mathlib.CategoryTheory.Adjunction.Limits (4.2s)
✔ [3103/3145] Built Mathlib.LinearAlgebra.LinearDisjoint (5.1s)
✔ [3104/3154] Built Mathlib.CategoryTheory.Limits.Preserves.Limits (2.0s)
✔ [3105/3154] Built Mathlib.CategoryTheory.Functor.Currying (4.8s)
✔ [3106/3154] Built Mathlib.CategoryTheory.Limits.Types.Limits (2.2s)
✔ [3107/3154] Built Mathlib.CategoryTheory.Limits.Types.ColimitType (2.4s)
✔ [3108/3163] Built Mathlib.CategoryTheory.ShrinkYoneda (3.6s)
✔ [3109/3163] Built Mathlib.CategoryTheory.Limits.Types.Yoneda (3.5s)
✔ [3110/3165] Built Mathlib.CategoryTheory.Limits.Types.Colimits (2.1s)
✔ [3111/3165] Built Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (5.7s)
✔ [3112/3168] Built Mathlib.CategoryTheory.Limits.Preserves.Ulift (1.3s)
✔ [3113/3168] Built Mathlib.CategoryTheory.MorphismProperty.Composition (2.4s)
✔ [3114/3168] Built Mathlib.CategoryTheory.Comma.Over.Basic (21s)
✔ [3115/3170] Built Mathlib.CategoryTheory.Limits.Yoneda (2.1s)
✔ [3116/3170] Built Mathlib.Algebra.Module.LocalizedModule.AtPrime (1.4s)
✔ [3117/3170] Built Mathlib.LinearAlgebra.TensorProduct.Pi (3.4s)
✔ [3118/3172] Built Mathlib.CategoryTheory.MorphismProperty.Concrete (1.4s)
✔ [3119/3172] Built Mathlib.RingTheory.LocalProperties.Submodule (3.3s)
✔ [3120/3172] Built Mathlib.RingTheory.SurjectiveOnStalks (4.3s)
✔ [3121/3172] Built Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (4.0s)
✔ [3122/3175] Built Mathlib.RingTheory.Finiteness.Nakayama (2.5s)
✔ [3123/3175] Built Mathlib.RingTheory.LocalProperties.Exactness (7.7s)
✔ [3124/3175] Built Mathlib.RingTheory.Nakayama (3.4s)
✔ [3125/3175] Built Mathlib.Algebra.Module.LocalizedModule.Int (1.9s)
✔ [3126/3178] Built Mathlib.RingTheory.LocalRing.ResidueField.Ideal (5.9s)
✔ [3127/3178] Built Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (11s)
✔ [3128/3178] Built Mathlib.RingTheory.Localization.Finiteness (3.6s)
✔ [3129/3182] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (3.8s)
✔ [3130/3182] Built Mathlib.RingTheory.QuotSMulTop (4.7s)
✔ [3131/3182] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts (1.7s)
✔ [3132/3183] Built Mathlib.Algebra.Category.Ring.Basic (5.7s)
✔ [3133/3183] Built Mathlib.Algebra.Category.MonCat.ForgetCorepresentable (1.4s)
✔ [3134/3183] Built Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso (1.1s)
✔ [3135/3190] Built Mathlib.Algebra.Category.Ring.Instances (1.7s)
✔ [3136/3190] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (3.4s)
✔ [3137/3191] Built Mathlib.Algebra.Ring.Shrink (1.2s)
✔ [3138/3197] Built Mathlib.Algebra.Category.MonCat.Limits (4.5s)
✔ [3139/3198] Built Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (1.5s)
✔ [3140/3198] Built Mathlib.CategoryTheory.Category.Cat.AsSmall (1.2s)
✔ [3141/3198] Built Mathlib.Algebra.Category.Ring.Colimits (3.9s)
✔ [3142/3206] Built Mathlib.CategoryTheory.IsConnected (2.2s)
✔ [3143/3210] Built Mathlib.CategoryTheory.Limits.Types.Products (2.3s)
✔ [3144/3210] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (5.3s)
✔ [3145/3210] Built Mathlib.CategoryTheory.Functor.TwoSquare (2.3s)
✔ [3146/3210] Built Mathlib.CategoryTheory.Monad.Basic (3.9s)
✔ [3147/3214] Built Mathlib.CategoryTheory.Elements (6.3s)
✔ [3148/3214] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (2.1s)
✔ [3149/3214] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (4.7s)
✔ [3150/3214] Built Mathlib.CategoryTheory.Monad.Algebra (4.3s)
✔ [3151/3223] Built Mathlib.CategoryTheory.Limits.Shapes.Equalizers (8.6s)
✔ [3152/3223] Built Mathlib.CategoryTheory.Adjunction.Mates (6.3s)
✔ [3153/3223] Built Mathlib.CategoryTheory.EffectiveEpi.Basic (1.9s)
✔ [3154/3223] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (2.9s)
✔ [3155/3223] Built Mathlib.CategoryTheory.Monad.Products (2.8s)
✔ [3156/3223] Built Mathlib.CategoryTheory.Limits.Connected (2.0s)
✔ [3157/3223] Built Mathlib.CategoryTheory.Grothendieck (8.6s)
✔ [3158/3228] Built Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (1.6s)
✔ [3159/3228] Built Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (2.0s)
✔ [3160/3228] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (5.3s)
✔ [3161/3228] Built Mathlib.CategoryTheory.Limits.Shapes.Images (5.5s)
✔ [3162/3228] Built Mathlib.CategoryTheory.Comma.Over.Pullback (5.3s)
✔ [3163/3228] Built Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (3.5s)
✔ [3164/3228] Built Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts (1.2s)
✔ [3165/3229] Built Mathlib.RingTheory.SimpleRing.Field (2.0s)
✔ [3166/3229] Built Mathlib.CategoryTheory.Filtered.Basic (3.0s)
✔ [3167/3229] Built FLT.Mathlib.Algebra.FixedPoints.Basic (2.6s)
✔ [3168/3229] Built Mathlib.CategoryTheory.Limits.Types.Images (1.5s)
✔ [3169/3230] Built Mathlib.CategoryTheory.Limits.Opposites (4.3s)
✔ [3170/3230] Built Mathlib.RingTheory.SimpleRing.Principal (1.3s)
✔ [3171/3230] Built Mathlib.CategoryTheory.Limits.Preserves.Finite (1.9s)
✔ [3172/3230] Built Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (4.1s)
✔ [3173/3230] Built Mathlib.CategoryTheory.Filtered.Connected (1.3s)
✔ [3174/3230] Built Mathlib.Algebra.Order.Ring.IsNonarchimedean (2.8s)
✔ [3175/3230] Built Mathlib.Data.Int.WithZero (1.6s)
✔ [3176/3230] Built Mathlib.CategoryTheory.Limits.Types.Filtered (2.4s)
✔ [3177/3230] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (2.1s)
✔ [3178/3230] Built Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (4.7s)
✔ [3179/3230] Built Mathlib.CategoryTheory.Limits.ExactFunctor (4.1s)
✔ [3180/3230] Built Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic (1.9s)
✔ [3181/3230] Built Mathlib.CategoryTheory.Limits.Final (8.6s)
✔ [3182/3230] Built Mathlib.Algebra.Category.ModuleCat.Semi (3.8s)
✔ [3183/3232] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (3.5s)
✔ [3184/3232] Built Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers (4.1s)
✔ [3185/3232] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs (2.8s)
✔ [3186/3232] Built Mathlib.CategoryTheory.Limits.Constructions.EpiMono (1.3s)
✔ [3187/3232] Built Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (2.1s)
✔ [3188/3234] Built Mathlib.RingTheory.FiniteLength (2.1s)
✔ [3189/3234] Built Mathlib.CategoryTheory.ConcreteCategory.EpiMono (1.6s)
✔ [3190/3238] Built Mathlib.CategoryTheory.Limits.Shapes.RegularMono (4.1s)
✔ [3191/3238] Built Mathlib.CategoryTheory.Limits.Shapes.Kernels (10s)
✔ [3192/3238] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (4.1s)
✔ [3193/3239] Built Mathlib.Algebra.GroupWithZero.Submonoid.Instances (1.5s)
✔ [3194/3242] Built Mathlib.Algebra.Order.GroupWithZero.WithZero (1.4s)
✔ [3195/3242] Built Mathlib.RingTheory.Length (3.9s)
✔ [3196/3242] Built Mathlib.CategoryTheory.Limits.Shapes.KernelPair (2.0s)
✔ [3197/3242] Built Mathlib.RingTheory.Bezout (1.6s)
✔ [3198/3245] Built Mathlib.CategoryTheory.Preadditive.Basic (4.1s)
✔ [3199/3245] Built Mathlib.Algebra.GroupWithZero.Range (3.3s)
✔ [3200/3245] Built Mathlib.CategoryTheory.Preadditive.FunctorCategory (1.8s)
✔ [3201/3245] Built Mathlib.Algebra.Category.Grp.Preadditive (1.8s)
✔ [3202/3245] Built Mathlib.CategoryTheory.Linear.Basic (2.4s)
✔ [3203/3245] Built Mathlib.RingTheory.ReesAlgebra (2.0s)
✔ [3204/3247] Built Mathlib.CategoryTheory.Limits.Shapes.Biproducts (9.2s)
✔ [3205/3247] Built Mathlib.Algebra.Order.GroupWithZero.Range (1.7s)
✔ [3206/3247] Built Mathlib.Algebra.Category.Grp.ForgetCorepresentable (1.6s)
✔ [3207/3248] Built Mathlib.CategoryTheory.Limits.Shapes.Diagonal (7.5s)
✔ [3208/3249] Built Mathlib.RingTheory.Jacobson.Polynomial (2.1s)
✔ [3209/3249] Built Mathlib.RingTheory.Filtration (5.2s)
✔ [3210/3249] Built Mathlib.CategoryTheory.MorphismProperty.Limits (5.9s)
✔ [3211/3249] Built Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (10s)
✔ [3212/3250] Built Mathlib.Algebra.Category.Grp.Limits (8.4s)
✔ [3213/3250] Built Mathlib.Algebra.Order.Ring.Idempotent (2.2s)
✔ [3214/3250] Built Mathlib.Order.Heyting.Hom (3.9s)
✔ [3215/3250] Built Mathlib.CategoryTheory.Preadditive.Projective.Basic (2.8s)
✔ [3216/3250] Built Mathlib.RingTheory.Valuation.Basic (15s)
✔ [3217/3250] Built Mathlib.RingTheory.Jacobson.Ring (7.5s)
✔ [3218/3253] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts (2.9s)
✔ [3219/3253] Built Mathlib.RingTheory.Ideal.MinimalPrime.Localization (2.5s)
✔ [3220/3253] Built Mathlib.RingTheory.Ideal.Cotangent (8.2s)
✔ [3221/3253] Built Mathlib.RingTheory.Valuation.PrimeMultiplicity (1.3s)
✔ [3222/3253] Built Mathlib.CategoryTheory.Preadditive.Injective.Basic (2.4s)
✔ [3223/3253] Built Mathlib.RingTheory.Localization.AsSubring (2.7s)
✔ [3224/3254] Built Mathlib.RingTheory.Valuation.Integers (5.1s)
✔ [3225/3254] Built Mathlib.RingTheory.Spectrum.Prime.RingHom (4.3s)
✔ [3226/3254] Built Mathlib.RingTheory.Valuation.ValuationRing (4.7s)
✔ [3227/3257] Built Mathlib.CategoryTheory.Preadditive.Biproducts (8.7s)
✔ [3228/3257] Built Mathlib.Algebra.Category.Ring.Limits (16s)
✔ [3229/3257] Built Mathlib.RingTheory.Spectrum.Maximal.Localization (4.4s)
✔ [3230/3258] Built Mathlib.RingTheory.DiscreteValuationRing.Basic (4.2s)
✔ [3231/3258] Built Mathlib.Topology.Sets.OpenCover (1.6s)
✔ [3232/3261] Built Mathlib.Order.BooleanSubalgebra (7.0s)
✔ [3233/3261] Built Mathlib.Topology.LocallyClosed (1.7s)
✔ [3234/3261] Built Mathlib.CategoryTheory.Preadditive.AdditiveFunctor (3.2s)
✔ [3235/3267] Built Mathlib.Topology.Spectral.Hom (1.6s)
✔ [3236/3267] Built Mathlib.Topology.LocalAtTarget (2.6s)
✔ [3237/3267] Built Mathlib.Order.Ideal (3.5s)
✔ [3238/3267] Built Mathlib.CategoryTheory.Linear.LinearFunctor (2.2s)
✔ [3239/3269] Built Mathlib.CategoryTheory.Monoidal.Preadditive (4.7s)
✔ [3240/3272] Built Mathlib.Algebra.Category.Ring.Constructions (8.7s)
✔ [3241/3272] Built Mathlib.Topology.Sober (2.1s)
✔ [3242/3272] Built Mathlib.Topology.Spectral.Prespectral (2.1s)
✔ [3243/3272] Built Mathlib.Algebra.Category.ModuleCat.Basic (8.1s)
✔ [3244/3272] Built Mathlib.Topology.KrullDimension (1.3s)
✔ [3245/3273] Built Mathlib.CategoryTheory.Monoidal.Linear (1.0s)
✔ [3246/3273] Built Mathlib.RingTheory.Valuation.ExtendToLocalization (2.3s)
✔ [3247/3273] Built Mathlib.Topology.Spectral.Basic (1.8s)
✔ [3248/3273] Built Mathlib.RingTheory.RingHomProperties (3.4s)
✔ [3249/3273] Built Mathlib.RingTheory.ChainOfDivisors (3.2s)
✔ [3250/3273] Built Mathlib.Algebra.Category.ModuleCat.EpiMono (1.8s)
✔ [3251/3274] Built Mathlib.Algebra.Category.Grp.ZModuleEquivalence (1.6s)
✔ [3252/3274] Built Mathlib.Algebra.Order.Hom.Units (1.2s)
✔ [3253/3274] Built Mathlib.Topology.Constructible (3.4s)
✔ [3254/3274] Built Mathlib.Algebra.Category.ModuleCat.Injective (1.6s)
✔ [3255/3274] Built Mathlib.RingTheory.LocalProperties.Basic (5.4s)
✔ [3256/3274] Built Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (8.1s)
✔ [3257/3274] Built Mathlib.Algebra.Category.Grp.Injective (1.7s)
✔ [3258/3274] Built Mathlib.RingTheory.LocalProperties.IntegrallyClosed (3.1s)
✔ [3259/3274] Built Mathlib.RingTheory.Spectrum.Prime.Topology (8.0s)
✔ [3260/3278] Built Mathlib.RingTheory.Valuation.ValuativeRel.Basic (12s)
✔ [3261/3278] Built Mathlib.RingTheory.Support (3.9s)
✔ [3262/3278] Built Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric (2.5s)
✔ [3263/3280] Built Mathlib.RingTheory.KrullDimension.Zero (2.2s)
✔ [3264/3280] Built Mathlib.Topology.Algebra.UniformFilterBasis (1.6s)
✔ [3265/3282] Built Mathlib.Algebra.Module.CharacterModule (5.5s)
✔ [3266/3285] Built Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (20s)
✔ [3267/3285] Built Mathlib.Topology.Algebra.OpenSubgroup (4.2s)
✔ [3268/3285] Built Mathlib.RingTheory.DiscreteValuationRing.TFAE (3.3s)
✔ [3269/3285] Built Mathlib.Topology.Algebra.WithZeroTopology (2.0s)
✔ [3270/3285] Built Mathlib.RingTheory.Flat.Tensor (2.5s)
✔ [3271/3286] Built Mathlib.Topology.Algebra.Nonarchimedean.Basic (2.1s)
✔ [3272/3286] Built Mathlib.RingTheory.DedekindDomain.Dvr (2.3s)
✔ [3273/3287] Built Mathlib.Topology.Algebra.Nonarchimedean.Bases (2.6s)
✔ [3274/3290] Built Mathlib.RingTheory.Finiteness.Quotient (1.9s)
✔ [3275/3290] Built Mathlib.Algebra.CharP.Quotient (1.7s)
✔ [3276/3293] Built Mathlib.RingTheory.Valuation.ValuationSubring (9.1s)
✔ [3277/3293] Built Mathlib.Data.ZMod.ValMinAbs (2.1s)
✔ [3278/3294] Built Mathlib.RingTheory.Flat.EquationalCriterion (6.3s)
✔ [3279/3297] Built Mathlib.LinearAlgebra.FreeModule.Determinant (1.5s)
✔ [3280/3297] Built Mathlib.Data.Int.Associated (968ms)
✔ [3281/3297] Built Mathlib.Data.Int.NatAbs (773ms)
✔ [3282/3297] Built Mathlib.RingTheory.Ideal.Basis (1.8s)
✔ [3283/3300] Built Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (2.3s)
✔ [3284/3302] Built Mathlib.FieldTheory.Finite.Basic (6.5s)
✔ [3285/3302] Built Mathlib.Topology.Algebra.Valued.ValuationTopology (8.4s)
✔ [3286/3304] Built Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (3.6s)
✔ [3287/3304] Built Mathlib.Algebra.GroupWithZero.Torsion (1.6s)
✔ [3288/3304] Built Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp (1.3s)
✔ [3289/3304] Built Mathlib.RingTheory.LocalRing.Module (13s)
✔ [3290/3308] Built Mathlib.RingTheory.Ideal.Norm.AbsNorm (4.9s)
✔ [3291/3318] Built Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (5.6s)
✔ [3292/3318] Built Mathlib.NumberTheory.RamificationInertia.Ramification (5.2s)
✔ [3293/3318] Built Mathlib.Topology.Algebra.RestrictedProduct.Basic (5.6s)
✔ [3294/3323] Built Mathlib.Algebra.Group.Pi.Units (903ms)
✔ [3295/3323] Built Mathlib.NumberTheory.RamificationInertia.Inertia (3.9s)
✔ [3296/3323] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (2.0s)
✔ [3297/3323] Built Mathlib.Algebra.FiveLemma (5.1s)
✔ [3298/3323] Built FLT.Mathlib.Order.Filter.Cofinite (1.2s)
✔ [3299/3323] Built FLT.Mathlib.Topology.Algebra.Group.Units (1.7s)
✔ [3300/3323] Built FLT.Mathlib.Topology.Bases (1.3s)
✔ [3301/3323] Built Mathlib.Topology.Algebra.Valued.ValuedField (21s)
✔ [3302/3323] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (3.9s)
✔ [3303/3323] Built Mathlib.Topology.Algebra.RestrictedProduct.Units (1.9s)
✔ [3304/3323] Built Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (3.6s)
✔ [3305/3323] Built Mathlib.Topology.Algebra.Group.Units (1.5s)
✔ [3306/3323] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (1.3s)
✔ [3307/3323] Built Mathlib.RingTheory.PicardGroup (18s)
✔ [3308/3324] Built FLT.Mathlib.MeasureTheory.Group.Action (2.4s)
✔ [3309/3324] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (1.8s)
✔ [3310/3324] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (5.5s)
✔ [3311/3324] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (2.4s)
✔ [3312/3324] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (9.2s)
✔ [3313/3324] Built Mathlib.NumberTheory.RamificationInertia.Basic (12s)
✔ [3314/3325] Built FLT.Mathlib.MeasureTheory.Group.Measure (1.8s)
✔ [3315/3325] Built Mathlib.Topology.Algebra.Valued.WithVal (12s)
✔ [3316/3328] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (5.9s)
✔ [3317/3329] Built Mathlib.MeasureTheory.Group.Integral (3.4s)
✔ [3318/3329] Built Mathlib.Analysis.Normed.Affine.AddTorsor (4.1s)
✔ [3319/3329] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (8.3s)
✔ [3320/3337] Built FLT.Hacks.RightActionInstances (7.0s)
✔ [3321/3337] Built Mathlib.Topology.ContinuousMap.Ordered (1.8s)
✔ [3322/3344] Built Mathlib.LinearAlgebra.AffineSpace.Ordered (6.3s)
✔ [3323/3344] Built Mathlib.RingTheory.DedekindDomain.Factorization (14s)
✔ [3324/3344] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.3s)
✔ [3325/3344] Built Mathlib.Data.DFinsupp.Encodable (1.5s)
✔ [3326/3345] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.6s)
✔ [3327/3345] Built Mathlib.RingTheory.DedekindDomain.AdicValuation (14s)
✔ [3328/3345] Built Mathlib.Topology.UrysohnsLemma (3.4s)
✔ [3329/3348] Built Mathlib.Data.Finsupp.Encodable (1.1s)
✔ [3330/3348] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (1.7s)
✔ [3331/3349] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.4s)
✔ [3332/3349] Built Mathlib.Algebra.Order.Group.Cyclic (1.6s)
✔ [3333/3349] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (1.7s)
✔ [3334/3349] Built Mathlib.Topology.Metrizable.Urysohn (1.8s)
✔ [3335/3349] Built Mathlib.LinearAlgebra.Countable (1.3s)
✔ [3336/3354] Built Mathlib.MeasureTheory.Measure.EverywherePos (2.9s)
✔ [3337/3354] Built Mathlib.Algebra.Group.Int.TypeTags (809ms)
✔ [3338/3355] Built Mathlib.RingTheory.Ideal.Oka (1.5s)
✔ [3339/3355] Built FLT.Mathlib.LinearAlgebra.Countable (1.6s)
✔ [3340/3355] Built Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (6.4s)
✔ [3341/3355] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (1.6s)
✔ [3342/3355] Built Mathlib.Data.Real.Embedding (3.8s)
✔ [3343/3355] Built Mathlib.RingTheory.PrincipalIdealDomainOfPrime (1.7s)
✔ [3344/3356] Built Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient (1.9s)
✔ [3345/3356] Built Mathlib.RingTheory.Valuation.RankOne (4.9s)
✔ [3346/3360] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (5.8s)
✔ [3347/3360] Built Mathlib.MeasureTheory.Measure.Haar.Unique (10s)
✔ [3348/3361] Built Mathlib.Order.Interval.Finset.DenselyOrdered (1.2s)
✔ [3349/3362] Built Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (4.6s)
✔ [3350/3362] Built Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (3.7s)
✔ [3351/3362] Built Mathlib.RingTheory.Valuation.Discrete.Basic (5.7s)
✔ [3352/3366] Built Mathlib.Algebra.Order.Archimedean.Submonoid (1.2s)
✔ [3353/3366] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (12s)
✔ [3354/3366] Built Mathlib.Topology.MetricSpace.Ultra.Basic (1.6s)
✔ [3355/3366] Built Mathlib.RingTheory.Valuation.Discrete.RankOne (3.6s)
✔ [3356/3372] Built Mathlib.Analysis.Normed.Group.Ultra (3.4s)
✔ [3357/3372] Built FLT.HaarMeasure.HaarChar.AddEquiv (7.2s)
✔ [3358/3373] Built Mathlib.GroupTheory.ArchimedeanDensely (8.1s)
✔ [3359/3380] Built Mathlib.NumberTheory.Padics.PadicVal.Basic (3.9s)
✔ [3360/3380] Built Mathlib.Topology.Algebra.Valued.NormedValued (6.1s)
✔ [3361/3380] Built FLT.HaarMeasure.HaarChar.Ring (5.8s)
✔ [3362/3382] Built Mathlib.Topology.Algebra.Valued.WithZeroMulInt (2.8s)
✔ [3363/3382] Built Mathlib.RingTheory.Valuation.Archimedean (3.9s)
✔ [3364/3382] Built Mathlib.Analysis.Normed.Field.ProperSpace (2.6s)
✔ [3365/3382] Built Mathlib.NumberTheory.Padics.PadicNorm (2.4s)
✔ [3366/3382] Built FLT.Mathlib.RingTheory.Localization.BaseChange (2.8s)
✔ [3367/3382] Built FLT.DedekindDomain.AdicValuation (14s)
✔ [3368/3382] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (3.4s)
✔ [3369/3384] Built Mathlib.NumberTheory.NumberField.Completion.InfinitePlace (8.4s)
✔ [3370/3384] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (1.9s)
✔ [3371/3386] Built Mathlib.NumberTheory.Padics.PadicNumbers (8.9s)
✔ [3372/3386] Built FLT.DedekindDomain.IntegralClosure (9.0s)
✔ [3373/3391] Built Mathlib.LinearAlgebra.Dimension.OrzechProperty (4.4s)
✔ [3374/3400] Built Mathlib.NumberTheory.NumberField.Completion.FinitePlace (14s)
✔ [3375/3400] Built Mathlib.NumberTheory.Padics.PadicIntegers (5.2s)
✔ [3376/3400] Built Mathlib.RingTheory.FractionalIdeal.Norm (4.2s)
✔ [3377/3400] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (1.8s)
✔ [3378/3400] Built Mathlib.RingTheory.RootsOfUnity.Complex (2.8s)
✔ [3379/3400] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (1.4s)
✔ [3380/3410] Built FLT.Mathlib.Algebra.Algebra.Hom (3.2s)
✔ [3381/3410] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (3.0s)
✔ [3382/3410] Built Mathlib.NumberTheory.Padics.RingHoms (5.9s)
✔ [3383/3410] Built Mathlib.NumberTheory.NumberField.FractionalIdeal (3.8s)
✔ [3384/3410] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.9s)
✔ [3385/3410] Built Mathlib.NumberTheory.Padics.WithVal (7.8s)
✔ [3386/3410] Built Mathlib.Algebra.Module.ZLattice.Basic (13s)
✔ [3387/3410] Built FLT.Mathlib.Algebra.Algebra.Pi (1.7s)
✔ [3388/3410] Built FLT.Mathlib.Algebra.Algebra.Bilinear (2.4s)
✔ [3389/3410] Built Mathlib.RingTheory.Flat.Stability (1.9s)
✔ [3390/3410] Built Mathlib.NumberTheory.NumberField.Units.Basic (5.6s)
✔ [3391/3411] Built FLT.Mathlib.Topology.Algebra.MulAction (1.2s)
✔ [3392/3414] Built FLT.Mathlib.Algebra.IsDirectLimit (2.5s)
✔ [3393/3414] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (1.9s)
✔ [3394/3414] Built FLT.Mathlib.LinearAlgebra.Pi (1.6s)
✔ [3395/3414] Built Mathlib.NumberTheory.Padics.ProperSpace (1.6s)
✔ [3396/3414] Built Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (6.9s)
✔ [3397/3414] Built Mathlib.RingTheory.Flat.Localization (3.7s)
✔ [3398/3414] Built Mathlib.NumberTheory.Padics.HeightOneSpectrum (12s)
✔ [3399/3414] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (2.0s)
✔ [3400/3416] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (12s)
✔ [3401/3416] Built Mathlib.RingTheory.Ideal.IsPrincipal (2.5s)
✔ [3402/3416] Built FLT.NumberField.Completion.Finite (2.7s)
✔ [3403/3429] Built FLT.NumberField.HeightOneSpectrum (2.2s)
✔ [3404/3429] Built Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (17s)
✔ [3405/3430] Built Mathlib.RingTheory.Flat.TorsionFree (2.9s)
✔ [3406/3430] Built Mathlib.Topology.Algebra.NonUnitalAlgebra (3.6s)
✔ [3407/3430] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (4.4s)
✔ [3408/3430] Built Mathlib.Topology.Algebra.StarSubalgebra (4.2s)
✔ [3409/3430] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (1.7s)
✔ [3410/3430] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (1.7s)
✔ [3411/3430] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (10s)
✔ [3412/3430] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (1.5s)
✔ [3413/3430] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (1.4s)
✔ [3414/3433] Built FLT.Mathlib.Topology.Constructions (1.5s)
✔ [3415/3433] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (1.9s)
✔ [3416/3433] Built FLT.NumberField.InfinitePlace.Extension (4.1s)
✔ [3417/3433] Built Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (4.3s)
✔ [3418/3433] Built Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances (4.8s)
✔ [3419/3440] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (2.7s)
✔ [3420/3440] Built Mathlib.Topology.Algebra.NonUnitalStarAlgebra (5.5s)
✔ [3421/3442] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (3.4s)
✔ [3422/3442] Built Mathlib.NumberTheory.NumberField.AdeleRing (3.0s)
✔ [3423/3442] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (4.1s)
✔ [3424/3442] Built Mathlib.LinearAlgebra.TensorProduct.Prod (4.8s)
✔ [3425/3442] Built FLT.NumberField.Padics.RestrictedProduct (3.7s)
✔ [3426/3442] Built Mathlib.NumberTheory.NumberField.Completion.Ramification (6.5s)
✔ [3427/3442] Built FLT.Mathlib.Data.Real.Archimedean (1.2s)
✔ [3428/3442] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (1.7s)
✔ [3429/3442] Built Mathlib.RingTheory.TwoSidedIdeal.Instances (1.2s)
✔ [3430/3442] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (2.9s)
✔ [3431/3445] Built Mathlib.RingTheory.TensorProduct.Pi (4.5s)
✔ [3432/3445] Built Mathlib.Analysis.CStarAlgebra.Classes (9.4s)
✔ [3433/3445] Built Mathlib.LinearAlgebra.Charpoly.Basic (3.2s)
✔ [3434/3445] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (2.0s)
✔ [3435/3448] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (9.2s)
✔ [3436/3448] Built Mathlib.LinearAlgebra.Charpoly.ToMatrix (3.0s)
✔ [3437/3448] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (2.6s)
✔ [3438/3448] Built Mathlib.RingTheory.SimpleRing.Congr (1.6s)
✔ [3439/3448] Built Mathlib.Order.CompleteSublattice (2.7s)
✔ [3440/3458] Built Mathlib.LinearAlgebra.Charpoly.BaseChange (2.1s)
✔ [3441/3460] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (2.2s)
✔ [3442/3461] Built Mathlib.GroupTheory.Congruence.BigOperators (1.6s)
✔ [3443/3467] Built FLT.DedekindDomain.Completion.BaseChange (58s)
✔ [3444/3467] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (3.1s)
✔ [3445/3470] Built Mathlib.RingTheory.SimpleModule.Isotypic (6.2s)
✔ [3446/3470] Built Mathlib.RingTheory.Complex (1.8s)
✔ [3447/3470] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (4.3s)
✔ [3448/3470] Built Mathlib.LinearAlgebra.Matrix.Ideal (3.4s)
✔ [3449/3470] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (1.4s)
✔ [3450/3473] Built FLT.NumberField.Completion.Infinite (29s)
✔ [3451/3473] Built Mathlib.NumberTheory.NumberField.ProductFormula (2.6s)
✔ [3452/3473] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (1.6s)
✔ [3453/3473] Built FLT.HaarMeasure.MeasurableSpacePadics (2.2s)
✔ [3454/3473] Built Mathlib.Algebra.Algebra.Subalgebra.Centralizer (2.0s)
✔ [3455/3473] Built Mathlib.RingTheory.SimpleRing.Matrix (1.5s)
✔ [3456/3473] Built FLT.HaarMeasure.HaarChar.RealComplex (2.8s)
✔ [3457/3473] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (2.9s)
✔ [3458/3473] Built Mathlib.GroupTheory.DoubleCoset (2.4s)
✔ [3459/3473] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.4s)
✔ [3460/3473] Built FLT.HaarMeasure.HaarChar.Padic (3.2s)
✔ [3461/3473] Built FLT.Mathlib.Algebra.Central.TensorProduct (3.3s)
✔ [3462/3473] Built FLT.Mathlib.GroupTheory.DoubleCoset (1.6s)
✔ [3463/3473] Built Mathlib.RingTheory.SimpleModule.WedderburnArtin (5.5s)
✔ [3464/3474] Built Mathlib.RingTheory.SimpleModule.IsAlgClosed (1.9s)
✔ [3465/3475] Built FLT.NumberField.InfiniteAdeleRing (17s)
✔ [3466/3478] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (9.6s)
✔ [3467/3478] Built FLT.Mathlib.LinearAlgebra.Determinant (6.3s)
✔ [3468/3478] Built Mathlib.Algebra.Order.Module.PositiveLinearMap (2.2s)
✔ [3469/3478] Built Mathlib.Topology.Algebra.Order.Support (1.7s)
✔ [3470/3484] Built Mathlib.Topology.Compactness.Paracompact (2.3s)
✔ [3471/3492] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (4.7s)
✔ [3472/3492] Built Mathlib.Topology.ShrinkingLemma (2.2s)
✔ [3473/3492] Built Mathlib.Order.Interval.Set.Union (1.2s)
✔ [3474/3492] Built Mathlib.Topology.ContinuousMap.ZeroAtInfty (7.4s)
✔ [3475/3492] Built Mathlib.Topology.Algebra.Group.Extension (1.4s)
✔ [3476/3492] Built FLT.Mathlib.Topology.HomToDiscrete (1.8s)
✔ [3477/3492] Built FLT.Mathlib.Topology.Polish (1.8s)
✔ [3478/3503] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (2.6s)
✔ [3479/3504] Built Mathlib.Topology.PartitionOfUnity (4.3s)
✔ [3480/3504] Built Mathlib.Algebra.Module.Torsion.Prod (940ms)
✔ [3481/3504] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (1.5s)
✔ [3482/3504] Built FLT.Mathlib.Topology.Instances.Matrix (1.5s)
✔ [3483/3504] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (2.4s)
✔ [3484/3504] Built Mathlib.Topology.ContinuousMap.CompactlySupported (10s)
✔ [3485/3504] Built Mathlib.NumberTheory.FLT.Basic (3.0s)
✔ [3486/3504] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (6.0s)
✔ [3487/3504] Built Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (3.9s)
✔ [3488/3507] Built Mathlib.MeasureTheory.Integral.CompactlySupported (2.4s)
✔ [3489/3507] Built Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (13s)
✔ [3490/3507] Built Mathlib.Data.Int.NatPrime (1.9s)
✔ [3491/3507] Built Mathlib.Algebra.Quaternion (23s)
✔ [3492/3507] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (49s)
✔ [3493/3508] Built Mathlib.NumberTheory.PythagoreanTriples (5.7s)
✔ [3494/3511] Built Mathlib.MeasureTheory.Measure.Haar.Extension (7.5s)
✔ [3495/3511] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (84s)
✔ [3496/3511] Built Mathlib.NumberTheory.FLT.Four (2.8s)
✔ [3497/3511] Built Mathlib.Combinatorics.Pigeonhole (2.2s)
✔ [3498/3514] Built Mathlib.Analysis.Quaternion (3.8s)
✔ [3499/3514] Built FLT.Mathlib.MeasureTheory.Haar.Extension (2.6s)
✔ [3500/3516] Built Mathlib.Algebra.Order.AbsoluteValue.Euclidean (1.2s)
✔ [3501/3516] Built Mathlib.Data.Int.AbsoluteValue (1.1s)
✔ [3502/3516] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (1.8s)
✔ [3503/3516] Built Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (1.8s)
✔ [3504/3517] Built Mathlib.LinearAlgebra.Matrix.AbsoluteValue (1.8s)
✔ [3505/3518] Built Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (1.7s)
✔ [3506/3518] Built Mathlib.Analysis.BoxIntegral.UnitPartition (5.1s)
✔ [3507/3520] Built Mathlib.Analysis.SpecialFunctions.Sqrt (2.0s)
✔ [3508/3520] Built Mathlib.NumberTheory.ClassNumber.Finite (5.9s)
✔ [3509/3520] Built FLT.QuaternionAlgebra.NumberField (11s)
✔ [3510/3520] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (6.0s)
✔ [3511/3526] Built Mathlib.Algebra.Module.ZLattice.Covolume (9.1s)
✔ [3512/3526] Built Mathlib.Analysis.Convex.Deriv (6.0s)
✔ [3513/3526] Built Mathlib.Analysis.Convex.SpecificFunctions.Deriv (3.0s)
✔ [3514/3527] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex (4.0s)
✔ [3515/3527] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (10s)
✔ [3516/3533] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv (1.8s)
✔ [3517/3533] Built Mathlib.Analysis.Convex.Body (4.8s)
✔ [3518/3533] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (5.3s)
✔ [3519/3533] Built Mathlib.LinearAlgebra.Matrix.FiniteDimensional (2.6s)
✔ [3520/3533] Built Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (7.9s)
✔ [3521/3533] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv (3.9s)
✔ [3522/3534] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (14s)
✔ [3523/3535] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (4.3s)
✔ [3524/3536] Built Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (6.9s)
✔ [3525/3536] Built FLT.NumberField.AdeleRing (44s)
✔ [3526/3536] Built Mathlib.Analysis.SpecialFunctions.Log.NegMulLog (2.9s)
✔ [3527/3536] Built Mathlib.Analysis.Normed.Affine.AddTorsorBases (2.9s)
✔ [3528/3536] Built Mathlib.Analysis.Real.Pi.Bounds (4.3s)
✔ [3529/3539] Built Mathlib.Analysis.Calculus.FDeriv.Extend (4.3s)
✔ [3530/3545] Built Mathlib.Analysis.Convex.Measure (2.0s)
✔ [3531/3547] Built Mathlib.Analysis.Calculus.Deriv.Prod (6.0s)
✔ [3532/3548] Built Mathlib.MeasureTheory.Group.GeometryOfNumbers (4.6s)
✔ [3533/3550] Built Mathlib.MeasureTheory.Integral.Layercake (5.7s)
✔ [3534/3550] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc (2.9s)
✔ [3535/3551] Built Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (9.2s)
✔ [3536/3552] Built Mathlib.MeasureTheory.Covering.VitaliFamily (2.6s)
✔ [3537/3552] Built Mathlib.MeasureTheory.Function.AEMeasurableOrder (2.0s)
✔ [3538/3554] Built FLT.HaarMeasure.HaarChar.AdeleRing (14s)
✔ [3539/3563] Built Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (3.6s)
✔ [3540/3563] Built Mathlib.MeasureTheory.Measure.Decomposition.Hahn (3.1s)
✔ [3541/3563] Built Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal (1.6s)
✔ [3542/3565] Built Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv (1.9s)
✔ [3543/3567] Built Mathlib.MeasureTheory.Integral.Average (8.3s)
✔ [3544/3567] Built Mathlib.MeasureTheory.Measure.Sub (1.8s)
✔ [3545/3567] Built Mathlib.MeasureTheory.Function.AEEqOfLIntegral (2.2s)
✔ [3546/3570] Built Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic (1.0s)
✔ [3547/3570] Built Mathlib.MeasureTheory.Measure.Lebesgue.Integral (2.3s)
✔ [3548/3570] Built Mathlib.MeasureTheory.Measure.Haar.NormedSpace (4.7s)
✔ [3549/3573] Built Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (6.2s)
✔ [3550/3573] Built Mathlib.MeasureTheory.Integral.Asymptotics (3.5s)
✔ [3551/3575] Built Mathlib.Topology.OpenPartialHomeomorph.Composition (2.9s)
✔ [3552/3575] Built Mathlib.Analysis.Analytic.Order (9.6s)
✔ [3553/3576] Built Mathlib.MeasureTheory.Covering.Differentiation (6.5s)
✔ [3554/3578] Built Mathlib.Data.Nat.Factorial.DoubleFactorial (1.7s)
✔ [3555/3578] Built Mathlib.Analysis.Complex.Convex (3.4s)
✔ [3556/3579] Built Mathlib.Algebra.Order.Field.Pointwise (1.2s)
✔ [3557/3581] Built Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (4.6s)
✔ [3558/3581] Built Mathlib.MeasureTheory.Covering.Besicovitch (7.3s)
✔ [3559/3586] Built Mathlib.Analysis.Meromorphic.Basic (10s)
✔ [3560/3587] Built Mathlib.MeasureTheory.Integral.Pi (3.5s)
✔ [3561/3587] Built Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv (3.4s)
✔ [3562/3587] Built Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (8.1s)
✔ [3563/3590] Built Mathlib.NumberTheory.NumberField.EquivReindex (4.5s)
✔ [3564/3590] Built Mathlib.Analysis.Calculus.ParametricIntegral (8.2s)
✔ [3565/3590] Built Mathlib.Data.Int.Log (3.2s)
✔ [3566/3592] Built Mathlib.Analysis.SpecialFunctions.Log.Base (6.7s)
✔ [3567/3594] Built Mathlib.Analysis.SpecialFunctions.Pow.Deriv (12s)
✔ [3568/3594] Built Mathlib.MeasureTheory.Function.Jacobian (11s)
✔ [3569/3594] Built Mathlib.FieldTheory.Galois.GaloisClosure (4.1s)
✔ [3570/3594] Built Mathlib.FieldTheory.KrullTopology (4.8s)
✔ [3571/3594] Built Mathlib.Analysis.SpecialFunctions.Integrability.Basic (4.4s)
✔ [3572/3595] Built Mathlib.Topology.Algebra.Group.ClosedSubgroup (2.4s)
✔ [3573/3595] Built Mathlib.Analysis.SpecialFunctions.JapaneseBracket (5.1s)
✔ [3574/3595] Built Mathlib.Analysis.SpecialFunctions.PolarCoord (6.0s)
✔ [3575/3601] Built Mathlib.MeasureTheory.Function.JacobianOneDim (6.8s)
✔ [3576/3601] Built Mathlib.RingTheory.Invariant.Defs (967ms)
✔ [3577/3601] Built Mathlib.RingTheory.RingHom.Finite (2.6s)
✔ [3578/3603] Built Mathlib.FieldTheory.Galois.Infinite (5.1s)
✔ [3579/3603] Built Mathlib.Data.Nat.Factorization.PrimePow (1.9s)
✔ [3580/3603] Built Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (8.3s)
✔ [3581/3603] Built Mathlib.Data.PNat.Prime (1.6s)
✔ [3582/3603] Built Mathlib.Analysis.SpecialFunctions.Integrals.Basic (7.8s)
✔ [3583/3607] Built FLT.DivisionAlgebra.Finiteness (75s)
✔ [3584/3607] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (3.0s)
✔ [3585/3607] Built Mathlib.MeasureTheory.Integral.IntegralEqImproper (12s)
✔ [3586/3607] Built Mathlib.MeasureTheory.Constructions.HaarToSphere (6.3s)
✔ [3587/3607] Built Mathlib.FieldTheory.RatFunc.Defs (2.6s)
✔ [3588/3607] Built Mathlib.RingTheory.Valuation.IsTrivialOn (2.3s)
✔ [3589/3609] Built Mathlib.RingTheory.IntegralClosure.IntegralRestrict (20s)
✔ [3590/3609] Built Mathlib.MeasureTheory.Integral.ExpDecay (1.8s)
✔ [3591/3616] Built Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (3.4s)
✔ [3592/3616] Built Mathlib.RingTheory.UniqueFactorizationDomain.Nat (1.6s)
✔ [3593/3616] Built Mathlib.Analysis.SpecialFunctions.Gamma.Basic (5.4s)
✔ [3594/3616] Built Mathlib.Analysis.MellinTransform (6.3s)
✔ [3595/3616] Built Mathlib.Tactic.ArithMult.Init (890ms)
✔ [3596/3616] Built Mathlib.RingTheory.Invariant.Basic (8.8s)
✔ [3597/3616] Built Mathlib.Data.Nat.Squarefree (3.6s)
✔ [3598/3621] Built Mathlib.MeasureTheory.Integral.Gamma (3.7s)
✔ [3599/3623] Built Mathlib.Tactic.ArithMult (1.2s)
✔ [3600/3623] Built Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (5.5s)
✔ [3601/3624] Built Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (5.2s)
✔ [3602/3624] Built Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (3.5s)
✔ [3603/3624] Built Mathlib.FieldTheory.Galois.Abelian (2.9s)
✔ [3604/3624] Built Mathlib.FieldTheory.RatFunc.Basic (22s)
✔ [3605/3624] Built Mathlib.NumberTheory.ArithmeticFunction.Defs (6.2s)
✔ [3606/3624] Built Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (5.6s)
✔ [3607/3624] Built Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (6.5s)
✔ [3608/3624] Built Mathlib.FieldTheory.Galois.IsGaloisGroup (14s)
✔ [3609/3624] Built Mathlib.RingTheory.Adjoin.PowerBasis (5.0s)
✔ [3610/3624] Built Mathlib.RingTheory.Polynomial.Eisenstein.Basic (2.3s)
✔ [3611/3624] Built Mathlib.NumberTheory.ArithmeticFunction.Zeta (2.6s)
✔ [3612/3630] Built Mathlib.FieldTheory.RatFunc.AsPolynomial (4.7s)
✔ [3613/3630] Built Mathlib.Algebra.GCDMonoid.IntegrallyClosed (2.9s)
✔ [3614/3634] Built Mathlib.Analysis.Normed.Module.Ray (2.7s)
✔ [3615/3635] Built Mathlib.NumberTheory.ArithmeticFunction.Misc (4.5s)
✔ [3616/3635] Built Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (9.3s)
✔ [3617/3635] Built Mathlib.NumberTheory.RamificationInertia.Galois (8.4s)
✔ [3618/3635] Built Mathlib.RingTheory.RootsOfUnity.Minpoly (2.5s)
✔ [3619/3638] Built Mathlib.Algebra.Algebra.ZMod (1.6s)
✔ [3620/3638] Built Mathlib.Analysis.Convex.StrictConvexSpace (2.0s)
✔ [3621/3638] Built Mathlib.NumberTheory.ArithmeticFunction.Moebius (2.8s)
✔ [3622/3640] Built Mathlib.Algebra.MonoidAlgebra.Cardinal (1.7s)
✔ [3623/3640] Built Mathlib.RingTheory.Algebraic.LinearIndependent (2.5s)
✔ [3624/3640] Built Mathlib.Analysis.Convex.Uniform (3.5s)
✔ [3625/3642] Built Mathlib.Algebra.MvPolynomial.Cardinal (2.6s)
✔ [3626/3644] Built Mathlib.GroupTheory.OreLocalization.Cardinality (2.4s)
✔ [3627/3644] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (5.9s)
✔ [3628/3644] Built Mathlib.Analysis.InnerProductSpace.Convex (2.4s)
✔ [3629/3647] Built Mathlib.NumberTheory.NumberField.Discriminant.Basic (8.9s)
✔ [3630/3647] Built Mathlib.RingTheory.OreLocalization.Cardinality (1.2s)
✔ [3631/3647] Built Mathlib.GroupTheory.MonoidLocalization.Cardinality (1.1s)
✔ [3632/3647] Built Mathlib.RingTheory.MvPolynomial (1.6s)
✔ [3633/3647] Built Mathlib.Analysis.Complex.Arg (1.7s)
✔ [3634/3650] Built Mathlib.Algebra.Polynomial.Cardinal (1.3s)
✔ [3635/3651] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (3.7s)
✔ [3636/3651] Built Mathlib.RingTheory.Localization.Cardinality (1.8s)
✔ [3637/3652] Built Mathlib.NumberTheory.NumberField.ClassNumber (3.7s)
✔ [3638/3653] Built Mathlib.RingTheory.Algebraic.Cardinality (1.9s)
✔ [3639/3653] Built Mathlib.Algebra.Ring.Subsemiring.MulOpposite (1.9s)
✔ [3640/3653] Built Mathlib.FieldTheory.MvRatFunc.Rank (2.1s)
✔ [3641/3653] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (2.4s)
✔ [3642/3656] Built Mathlib.Algebra.Polynomial.Basis (1.5s)
✔ [3643/3656] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (4.2s)
✔ [3644/3656] Built Mathlib.Algebra.Algebra.Subalgebra.Rank (5.9s)
✔ [3645/3656] Built Mathlib.Algebra.Ring.Subring.MulOpposite (2.3s)
✔ [3646/3656] Built Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality (3.7s)
✔ [3647/3657] Built Mathlib.RingTheory.TensorProduct.Nontrivial (2.8s)
✔ [3648/3658] Built Mathlib.Algebra.Algebra.Subalgebra.MulOpposite (2.2s)
✔ [3649/3659] Built Mathlib.RingTheory.Artinian.Ring (2.3s)
✔ [3650/3660] Built Mathlib.NumberTheory.Cyclotomic.Basic (12s)
✔ [3651/3661] Built Mathlib.RingTheory.LocalRing.ResidueField.Instances (4.6s)
✔ [3652/3661] Built Mathlib.RingTheory.Ideal.IdempotentFG (1.5s)
✔ [3653/3663] Built Mathlib.LinearAlgebra.TensorProduct.Subalgebra (14s)
✔ [3654/3664] Built Mathlib.RingTheory.FiniteStability (4.8s)
✔ [3655/3664] Built Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (6.5s)
✔ [3656/3667] Built Mathlib.RingTheory.Idempotents (6.0s)
✔ [3657/3667] Built Mathlib.RingTheory.Derivation.ToSquareZero (3.1s)
✔ [3658/3667] Built Mathlib.RingTheory.Localization.Away.AdjoinRoot (2.1s)
✔ [3659/3667] Built Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (2.9s)
✔ [3660/3670] Built Mathlib.Algebra.Algebra.Shrink (1.4s)
✔ [3661/3676] Built Mathlib.NumberTheory.Cyclotomic.Discriminant (5.4s)
✔ [3662/3679] Built Mathlib.RingTheory.MvPolynomial.Localization (3.7s)
✔ [3663/3681] Built Mathlib.RingTheory.LinearDisjoint (13s)
✔ [3664/3681] Built Mathlib.Algebra.Module.SnakeLemma (4.9s)
✔ [3665/3688] Built Mathlib.RingTheory.Extension.Basic (14s)
✔ [3666/3688] Built Mathlib.RingTheory.Spectrum.Prime.TensorProduct (3.1s)
✔ [3667/3689] Built Mathlib.GroupTheory.Submonoid.Inverses (3.2s)
✔ [3668/3689] Built Mathlib.RingTheory.Conductor (4.0s)
✔ [3669/3689] Built Mathlib.FieldTheory.LinearDisjoint (16s)
✔ [3670/3689] Built Mathlib.RingTheory.Kaehler.Basic (25s)
✔ [3671/3689] Built Mathlib.RingTheory.Localization.InvSubmonoid (2.0s)
✔ [3672/3689] Built Mathlib.RingTheory.Extension.Generators (15s)
✔ [3673/3694] Built Mathlib.RingTheory.FractionalIdeal.Extended (5.4s)
✔ [3674/3694] Built Mathlib.RingTheory.Kaehler.Polynomial (5.7s)
✔ [3675/3694] Built Mathlib.RingTheory.Unramified.Basic (5.0s)
✔ [3676/3697] Built Mathlib.RingTheory.Ideal.Quotient.Index (2.9s)
✔ [3677/3697] Built Mathlib.RingTheory.Extension.Presentation.Basic (6.9s)
✔ [3678/3700] Built Mathlib.RingTheory.LocalRing.Quotient (3.5s)
✔ [3679/3700] Built Mathlib.RingTheory.LocalRing.ResidueField.Fiber (16s)
✔ [3680/3700] Built Mathlib.RingTheory.Ideal.Int (2.6s)
✔ [3681/3700] Built Mathlib.RingTheory.DedekindDomain.PID (3.5s)
✔ [3682/3703] Built Mathlib.RingTheory.Unramified.Finite (7.1s)
✔ [3683/3706] Built Mathlib.RingTheory.Trace.Quotient (4.6s)
✔ [3684/3706] Built Mathlib.Data.Nat.Prime.Factorial (1.2s)
✔ [3685/3706] Built Mathlib.RingTheory.Prime (1.6s)
✔ [3686/3706] Built Mathlib.Data.Nat.Choose.Dvd (1.2s)
✔ [3687/3711] Built Mathlib.RingTheory.DedekindDomain.Instances (10s)
✔ [3688/3713] Built Mathlib.RingTheory.NormalClosure (13s)
✔ [3689/3713] Built Mathlib.RingTheory.Extension.Cotangent.Basic (15s)
✔ [3690/3716] Built Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (6.7s)
✔ [3691/3717] Built Mathlib.RingTheory.Fintype (1.7s)
✔ [3692/3717] Built Mathlib.Algebra.Ring.Divisibility.Lemmas (2.1s)
✔ [3693/3717] Built Mathlib.LinearAlgebra.Eigenspace.Basic (9.7s)
✔ [3694/3717] Built Mathlib.Tactic.ModCases (3.1s)
✔ [3695/3717] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (3.1s)
✔ [3696/3720] Built Mathlib.RingTheory.Ideal.Norm.RelNorm (12s)
✔ [3697/3720] Built Mathlib.LinearAlgebra.Matrix.Gershgorin (2.3s)
✔ [3698/3721] Built Mathlib.Topology.Separation.Profinite (3.1s)
✔ [3699/3721] Built Mathlib.Topology.Separation.Connected (1.5s)
✔ [3700/3721] Built Mathlib.Topology.Algebra.ClopenNhdofOne (1.6s)
✔ [3701/3722] Built Mathlib.RingTheory.Kaehler.JacobiZariski (16s)
✔ [3702/3726] Built Mathlib.Algebra.Category.Grp.FiniteGrp (1.5s)
✔ [3703/3726] Built Mathlib.CategoryTheory.FintypeCat (3.1s)
✔ [3704/3728] Built Mathlib.CategoryTheory.Adjunction.Reflective (2.7s)
✔ [3705/3728] Built Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (6.1s)
✔ [3706/3741] Built Mathlib.Topology.Compactification.StoneCech (1.0s)
✔ [3707/3741] Built Mathlib.RingTheory.Smooth.Kaehler (20s)
✔ [3708/3743] Built Mathlib.Topology.Category.TopCat.Basic (2.0s)
✔ [3709/3743] Built Mathlib.CategoryTheory.Monad.Adjunction (3.5s)
✔ [3710/3744] Built Mathlib.Topology.Category.TopCat.Adjunctions (1.2s)
✔ [3711/3744] Built Mathlib.Topology.Algebra.LinearTopology (2.9s)
✔ [3712/3744] Built Mathlib.Topology.Category.CompHausLike.Basic (1.0s)
✔ [3713/3745] Built Mathlib.Analysis.Normed.Unbundled.RingSeminorm (3.8s)
✔ [3714/3746] Built Mathlib.Topology.Category.TopCat.Limits.Basic (2.9s)
✔ [3715/3746] Built Mathlib.CategoryTheory.Monad.Limits (4.6s)
✔ [3716/3746] Built Mathlib.RingTheory.Smooth.Basic (9.9s)
✔ [3717/3746] Built Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (3.4s)
✔ [3718/3746] Built Mathlib.Analysis.Normed.Unbundled.AlgebraNorm (3.4s)
✔ [3719/3751] Built Mathlib.Algebra.Order.GroupWithZero.Bounds (937ms)
✔ [3720/3751] Built FLT.Deformations.Lemmas (5.6s)
✔ [3721/3752] Built Mathlib.Topology.MetricSpace.Sequences (1.3s)
✔ [3722/3754] Built Mathlib.Topology.Category.TopCat.Limits.Konig (1.5s)
✔ [3723/3754] Built Mathlib.Topology.Category.CompHaus.Basic (2.1s)
✔ [3724/3754] Built Mathlib.Algebra.Order.Group.DenselyOrdered (1.4s)
✔ [3725/3754] Built FLT.Deformations.RepresentationTheory.IntegralClosure (2.7s)
✔ [3726/3757] Built Mathlib.RingTheory.Etale.Basic (3.3s)
✔ [3727/3757] Built Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful (2.1s)
✔ [3728/3757] Built Mathlib.CategoryTheory.CofilteredSystem (2.6s)
✔ [3729/3757] Built Mathlib.Topology.Algebra.Order.LiminfLimsup (2.6s)
✔ [3730/3759] Built Mathlib.Topology.Category.Profinite.Basic (2.9s)
✔ [3731/3759] Built Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (3.4s)
✔ [3732/3759] Built Mathlib.Topology.Algebra.Group.TopologicalAbelianization (1.4s)
✔ [3733/3760] Built Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm (5.4s)
✔ [3734/3760] Built Mathlib.FieldTheory.AbsoluteGaloisGroup (1.8s)
✔ [3735/3761] Built Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic (7.8s)
✔ [3736/3761] Built Mathlib.RingTheory.Coalgebra.Basic (9.4s)
✔ [3737/3761] Built Mathlib.Analysis.Normed.Unbundled.FiniteExtension (4.1s)
✔ [3738/3765] Built Mathlib.RingTheory.Smooth.Pi (4.1s)
✔ [3739/3765] Built Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits (2.5s)
✔ [3740/3765] Built Mathlib.RingTheory.Unramified.Pi (3.2s)
✔ [3741/3766] Built Mathlib.RingTheory.Bialgebra.Basic (2.8s)
✔ [3742/3769] Built Mathlib.Analysis.Normed.Unbundled.InvariantExtension (2.9s)
✔ [3743/3769] Built Mathlib.RingTheory.Etale.Kaehler (18s)
✔ [3744/3770] Built Mathlib.RingTheory.Noetherian.Nilpotent (1.4s)
✔ [3745/3770] Built Mathlib.RingTheory.Finiteness.FiniteTypeLocal (3.5s)
✔ [3746/3770] Built Mathlib.RingTheory.Spectrum.Prime.Noetherian (2.6s)
✔ [3747/3770] Built Mathlib.LinearAlgebra.Matrix.Unique (2.4s)
✔ [3748/3770] Built Mathlib.RingTheory.Unramified.Locus (5.1s)
✔ [3749/3772] Built Mathlib.RingTheory.HopkinsLevitzki (4.1s)
✔ [3750/3772] Built Mathlib.Analysis.Normed.Unbundled.SpectralNorm (11s)
✔ [3751/3774] Built Mathlib.RingTheory.Finiteness.FinitePresentationLocal (6.7s)
✔ [3752/3777] Built Mathlib.RingTheory.Frobenius (3.6s)
✔ [3753/3777] Built Mathlib.RingTheory.Invariant.Profinite (15s)
✔ [3754/3777] Built Mathlib.RingTheory.Etale.Pi (2.0s)
✔ [3755/3777] Built Mathlib.RingTheory.Coalgebra.Hom (3.9s)
✔ [3756/3780] Built Mathlib.RingTheory.Unramified.Field (5.4s)
✔ [3757/3780] Built FLT.Deformations.RepresentationTheory.Frobenius (3.3s)
✔ [3758/3780] Built Mathlib.RingTheory.Bialgebra.Hom (5.4s)
✔ [3759/3780] Built Mathlib.RingTheory.Coalgebra.Equiv (5.0s)
✔ [3760/3780] Built Mathlib.RingTheory.Etale.Field (6.4s)
✔ [3761/3782] Built Mathlib.Algebra.WithConv (2.3s)
✔ [3762/3782] Built Mathlib.RingTheory.Unramified.LocalRing (5.0s)
✔ [3763/3783] Built Mathlib.RingTheory.Bialgebra.Equiv (6.2s)
✔ [3764/3786] Built FLT.Deformations.RepresentationTheory.Etale (11s)
✔ [3765/3789] Built Mathlib.RepresentationTheory.Basic (9.2s)
✔ [3766/3789] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (16s)
✔ [3767/3789] Built Mathlib.RepresentationTheory.AlgebraRepresentation.Basic (1.0s)
✔ [3768/3789] Built Mathlib.NumberTheory.RamificationInertia.Unramified (2.9s)
✔ [3769/3791] Built Mathlib.Topology.Instances.ZMod (1.0s)
✔ [3770/3791] Built Mathlib.RepresentationTheory.Subrepresentation (2.6s)
✔ [3771/3792] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (1.8s)
✔ [3772/3792] Built Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity (1.7s)
✔ [3773/3792] Built Mathlib.Analysis.Normed.Field.Approximation (3.9s)
✔ [3774/3795] Built Mathlib.RingTheory.Coalgebra.CoassocSimps (35s)
✔ [3775/3808] Built Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter (5.2s)
✔ [3776/3810] Built Mathlib.Analysis.Normed.Ring.Ultra (2.8s)
✔ [3777/3810] Built Mathlib.RepresentationTheory.Intertwining (13s)
✔ [3778/3810] Built Mathlib.FieldTheory.Minpoly.IsConjRoot (4.4s)
✔ [3779/3810] Built FLT.Data.Hurwitz (8.0s)
✔ [3780/3810] Built Mathlib.RingTheory.DedekindDomain.Different (25s)
✔ [3781/3810] Built Mathlib.RingTheory.Coalgebra.TensorProduct (16s)
✔ [3782/3810] Built FLT.Patching.Utils.InverseLimit (1.9s)
✔ [3783/3812] Built Mathlib.Analysis.Normed.Field.Ultra (1.0s)
✔ [3784/3812] Built Mathlib.Topology.Algebra.Module.Compact (1.4s)
✔ [3785/3812] Built FLT.Data.QHat (10s)
✔ [3786/3812] Built Mathlib.RepresentationTheory.Irreducible (2.5s)
✔ [3787/3813] Built FLT.Deformations.Algebra.InverseLimit.Basic (7.6s)
✔ [3788/3813] Built Mathlib.Analysis.Normed.Algebra.Ultra (1.6s)
✔ [3789/3819] Built Mathlib.Topology.Algebra.TopologicallyNilpotent (2.1s)
✔ [3790/3819] Built Mathlib.RingTheory.Coalgebra.Convolution (5.5s)
✔ [3791/3819] Built FLT.Data.HurwitzRatHat (3.3s)
✔ [3792/3819] Built FLT.Patching.Utils.Lemmas (6.4s)
✔ [3793/3832] Built Mathlib.RingTheory.Bialgebra.TensorProduct (11s)
✔ [3794/3832] Built Mathlib.RingTheory.DedekindDomain.LinearDisjoint (13s)
✔ [3795/3832] Built Mathlib.Topology.Algebra.Ring.Compact (2.3s)
✔ [3796/3832] Built FLT.Deformations.Algebra.InverseLimit.Topology (3.0s)
✔ [3797/3832] Built Mathlib.Analysis.Normed.Field.Krasner (3.3s)
✔ [3798/3832] Built Mathlib.Topology.Connected.Separation (1.3s)
✔ [3799/3832] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.4s)
✔ [3800/3832] Built Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (2.6s)
✔ [3801/3832] Built FLT.GaloisRepresentation.Cyclotomic (1.0s)
✔ [3802/3832] Built Mathlib.CategoryTheory.Subfunctor.Basic (2.5s)
✔ [3803/3832] Built FLT.Mathlib.RepresentationTheory.Basic (2.4s)
✔ [3804/3832] Built Mathlib.RingTheory.HopfAlgebra.Basic (3.7s)
✔ [3805/3832] Built FLT.Deformations.IsResidueAlgebra (2.1s)
✔ [3806/3832] Built FLT.Deformations.Subfunctor (1.6s)
✔ [3807/3832] Built Mathlib.Analysis.Normed.Field.Dense (4.8s)
✔ [3808/3837] Built FLT.Patching.Utils.AdicTopology (4.7s)
✔ [3809/3837] Built FLT.Deformations.RepresentationTheory.Irreducible (2.2s)
✔ [3810/3837] Built Mathlib.NumberTheory.NumberField.Discriminant.Different (7.2s)
✔ [3811/3838] Built FLT.Deformations.IsProartinian (2.2s)
✔ [3812/3838] Built Mathlib.NumberTheory.Padics.Complex (3.4s)
✔ [3813/3838] Built Mathlib.Algebra.Lie.Ideal (5.0s)
✔ [3814/3841] Built FLT.Deformations.Categories (4.6s)
✔ [3815/3842] Built Mathlib.Algebra.RingQuot (5.0s)
✔ [3816/3842] Built Mathlib.Algebra.Lie.IdealOperations (4.4s)
✔ [3817/3842] Built FLT.Deformations.RepresentationTheory.GaloisRep (18s)
✔ [3818/3844] Built Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (16s)
✔ [3819/3844] Built Mathlib.Analysis.Matrix.Normed (7.5s)
✔ [3820/3844] Built FLT.Deformations.LiftFunctor (4.8s)
✔ [3821/3844] Built FLT.GaloisRepresentation.Automorphic (3.6s)
✔ [3822/3844] Built Mathlib.Algebra.Lie.Abelian (6.1s)
✔ [3823/3844] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (2.1s)
✔ [3824/3844] Built FLT.EllipticCurve.Torsion (2.6s)
✔ [3825/3844] Built Mathlib.Algebra.TrivSqZeroExt.Basic (14s)
✔ [3826/3844] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.5s)
✔ [3827/3844] Built Mathlib.NumberTheory.NumberField.Cyclotomic.PID (2.9s)
✔ [3828/3844] Built Mathlib.Algebra.Lie.Prod (2.9s)
✔ [3829/3844] Built Mathlib.NumberTheory.NumberField.Cyclotomic.Three (4.2s)
✔ [3830/3844] Built FLT.Deformations.Representable (3.6s)
✔ [3831/3844] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.1s)
✔ [3832/3844] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (2.3s)
✔ [3833/3844] Built Mathlib.LinearAlgebra.TensorAlgebra.Basic (3.9s)
✔ [3834/3844] Built FLT.GaloisRepresentation.HardlyRamified.Lift (2.1s)
✔ [3835/3844] Built Mathlib.Algebra.Lie.TensorProduct (4.7s)
✔ [3836/3844] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.2s)
✔ [3837/3844] Built Mathlib.RingTheory.Derivation.Lie (3.1s)
✔ [3838/3846] Built Mathlib.Algebra.Lie.UniversalEnveloping (2.4s)
✔ [3839/3847] Built Mathlib.Data.Bundle (1.5s)
✔ [3840/3854] Built Mathlib.Analysis.RCLike.TangentCone (2.4s)
✔ [3841/3858] Built Mathlib.Topology.SeparatedMap (2.7s)
✔ [3842/3860] Built Mathlib.Geometry.Manifold.StructureGroupoid (3.4s)
✔ [3843/3860] Built Mathlib.Topology.IsLocalHomeomorph (2.1s)
✔ [3844/3866] Built Mathlib.NumberTheory.FLT.Three (9.5s)
✔ [3845/3875] Built Mathlib.Algebra.Lie.BaseChange (9.1s)
✔ [3846/3875] Built Mathlib.Topology.OpenPartialHomeomorph.Constructions (2.9s)
✔ [3847/3875] Built Mathlib.CategoryTheory.Monoidal.CoherenceLemmas (1.2s)
✔ [3848/3876] Built Mathlib.CategoryTheory.Adjunction.Parametrized (2.2s)
✔ [3849/3880] Built FLT.Basic.FreyPackage (3.3s)
✔ [3850/3880] Built Mathlib.Geometry.Manifold.ChartedSpace (3.5s)
✔ [3851/3881] Built Mathlib.Analysis.Normed.Operator.Prod (5.6s)
✔ [3852/3882] Built Mathlib.CategoryTheory.Preadditive.Opposite (2.4s)
✔ [3853/3885] Built Mathlib.CategoryTheory.Monoidal.Closed.Basic (3.6s)
✔ [3854/3885] Built FLT.GaloisRepresentation.HardlyRamified.Frey (1.9s)
✔ [3855/3885] Built Mathlib.Algebra.Category.Grp.Yoneda (2.1s)
✔ [3856/3886] Built Mathlib.Geometry.Manifold.HasGroupoid (2.6s)
✔ [3857/3886] Built Mathlib.CategoryTheory.Monoidal.Subcategory (3.3s)
✔ [3858/3886] Built Mathlib.LinearAlgebra.Coevaluation (3.2s)
✔ [3859/3886] Built FLT.Basic.Reductions (2.1s)
✔ [3860/3886] Built Mathlib.CategoryTheory.Monoidal.Rigid.Basic (6.4s)
✔ [3861/3886] Built Mathlib.CategoryTheory.Preadditive.Yoneda.Basic (3.5s)
✔ [3862/3888] Built Mathlib.Algebra.Category.ModuleCat.Limits (6.3s)
✔ [3863/3888] Built Mathlib.Geometry.Manifold.LocalInvariantProperties (3.7s)
✔ [3864/3889] Built Mathlib.Algebra.Category.ModuleCat.Products (2.4s)
✔ [3865/3889] Built Mathlib.CategoryTheory.Limits.Constructions.Equalizers (2.2s)
✔ [3866/3894] Built Mathlib.CategoryTheory.Linear.Yoneda (3.3s)
✔ [3867/3894] Built Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts (2.3s)
✔ [3868/3894] Built Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite (1.8s)
✔ [3869/3894] Built Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed (2.2s)
✔ [3870/3899] Built Mathlib.Geometry.Manifold.IsManifold.Basic (7.1s)
✔ [3871/3899] Built Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer (1.6s)
✔ [3872/3900] Built Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer (1.6s)
✔ [3873/3900] Built Mathlib.CategoryTheory.ConcreteCategory.Elementwise (1.2s)
✔ [3874/3900] Built Mathlib.LinearAlgebra.DirectSum.Finite (1.2s)
✔ [3875/3900] Built Mathlib.CategoryTheory.Monoidal.Rigid.Braided (1.9s)
✔ [3876/3902] Built Mathlib.Algebra.Category.FGModuleCat.Basic (4.1s)
✔ [3877/3902] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers (2.5s)
✔ [3878/3902] Built Mathlib.CategoryTheory.Limits.Constructions.Pullbacks (1.5s)
✔ [3879/3907] Built Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (6.9s)
✔ [3880/3907] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (3.1s)
✔ [3881/3907] Built Mathlib.Algebra.Category.Grp.Colimits (5.2s)
✔ [3882/3907] Built Mathlib.Geometry.Manifold.MFDeriv.Defs (3.1s)
✔ [3883/3907] Built Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (4.0s)
✔ [3884/3907] Built Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (3.7s)
✔ [3885/3908] Built Mathlib.CategoryTheory.Abelian.Images (2.5s)
✔ [3886/3908] Built Mathlib.Geometry.Manifold.ContMDiff.Defs (6.3s)
✔ [3887/3909] Built Mathlib.Algebra.Category.ModuleCat.Colimits (3.7s)
✔ [3888/3909] Built Mathlib.CategoryTheory.Limits.Skeleton (1.1s)
✔ [3889/3909] Built Mathlib.Algebra.Category.FGModuleCat.Limits (2.2s)
✔ [3890/3909] Built Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (3.7s)
✔ [3891/3909] Built Mathlib.Geometry.Manifold.ContMDiff.Basic (4.5s)
✔ [3892/3909] Built Mathlib.Algebra.Category.FGModuleCat.Colimits (3.1s)
✔ [3893/3909] Built Mathlib.CategoryTheory.Adjunction.Restrict (1.0s)
✔ [3894/3912] Built Mathlib.Geometry.Manifold.Notation (8.4s)
✔ [3895/3914] Built Mathlib.CategoryTheory.Abelian.NonPreadditive (3.8s)
✔ [3896/3914] Built Mathlib.CategoryTheory.ObjectProperty.Equivalence (1.3s)
✔ [3897/3914] Built Mathlib.CategoryTheory.ObjectProperty.Opposite (1.7s)
✔ [3898/3914] Built Mathlib.CategoryTheory.Limits.Presentation (2.1s)
✔ [3899/3918] Built Mathlib.Geometry.Manifold.ContMDiff.Constructions (7.0s)
✔ [3900/3918] Built Mathlib.CategoryTheory.ObjectProperty.Small (2.4s)
✔ [3901/3918] Built Mathlib.CategoryTheory.ObjectProperty.ContainsZero (1.3s)
✔ [3902/3918] Built Mathlib.Geometry.Manifold.MFDeriv.Basic (17s)
✔ [3903/3921] Built Mathlib.CategoryTheory.Abelian.Basic (7.8s)
✔ [3904/3928] Built Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape (1.9s)
✔ [3905/3931] Built Mathlib.CategoryTheory.ObjectProperty.Retract (1.7s)
✔ [3906/3935] Built Mathlib.CategoryTheory.Bicategory.Functor.Prelax (2.2s)
✔ [3907/3935] Built Mathlib.Tactic.CategoryTheory.ToApp (1.9s)
✔ [3908/3937] Built Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape (2.3s)
✔ [3909/3937] Built Mathlib.CategoryTheory.Bicategory.Functor.Oplax (4.4s)
✔ [3910/3937] Built Mathlib.CategoryTheory.Bicategory.Functor.Lax (5.1s)
✔ [3911/3937] Built Mathlib.CategoryTheory.Limits.FullSubcategory (1.6s)
✔ [3912/3939] Built Mathlib.Geometry.Manifold.ContMDiff.NormedSpace (13s)
✔ [3913/3940] Built Mathlib.Algebra.Category.ModuleCat.Kernels (2.8s)
✔ [3914/3940] Built Mathlib.Algebra.Algebra.Unitization (9.9s)
✔ [3915/3940] Built Mathlib.Geometry.Manifold.ContMDiffMap (2.7s)
✔ [3916/3942] Built Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence (1.4s)
✔ [3917/3942] Built Mathlib.Algebra.Category.ModuleCat.Abelian (2.0s)
✔ [3918/3942] Built Mathlib.CategoryTheory.Monoidal.FunctorCategory (4.6s)
✔ [3919/3942] Built Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor (8.2s)
✔ [3920/3942] Built Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory (2.2s)
✔ [3921/3947] Built Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (6.2s)
✔ [3922/3947] Built Mathlib.Geometry.Manifold.Algebra.Monoid (6.6s)
✔ [3923/3947] Built Mathlib.Combinatorics.Quiver.Cast (787ms)
✔ [3924/3947] Built Mathlib.FieldTheory.IsAlgClosed.Spectrum (2.6s)
✔ [3925/3949] Built Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (9.2s)
✔ [3926/3949] Built Mathlib.Geometry.Manifold.Algebra.LieGroup (3.8s)
✔ [3927/3949] Built Mathlib.Combinatorics.Quiver.SingleObj (932ms)
✔ [3928/3950] Built Mathlib.Geometry.Manifold.Algebra.SMul (3.8s)
✔ [3929/3950] Built Mathlib.CategoryTheory.Monoidal.Types.Basic (1.5s)
✔ [3930/3952] Built Mathlib.CategoryTheory.Limits.FunctorCategory.Finite (1.2s)
✔ [3931/3952] Built Mathlib.Geometry.Manifold.Algebra.Structures (1.0s)
✔ [3932/3956] Built Mathlib.CategoryTheory.SingleObj (1.9s)
✔ [3933/3956] Built Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra (2.4s)
✔ [3934/3972] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages (2.3s)
✔ [3935/3972] Built Mathlib.CategoryTheory.Preadditive.Transfer (1.3s)
✔ [3936/3972] Built Mathlib.CategoryTheory.Abelian.FunctorCategory (2.2s)
✔ [3937/3973] Built Mathlib.CategoryTheory.Linear.FunctorCategory (1.4s)
✔ [3938/3973] Built Mathlib.CategoryTheory.Action.Basic (5.0s)
✔ [3939/3973] Built FLT.GroupScheme.FiniteFlat (270ms)
✔ [3940/3973] Built Mathlib.RepresentationTheory.Equiv (4.1s)
✔ [3941/3973] Built Mathlib.CategoryTheory.WithTerminal.Basic (17s)
✔ [3942/3973] Built Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (6.4s)
✔ [3943/3973] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (1.6s)
✔ [3944/3973] Built FLT.Mathlib.Data.Set.Prod (550ms)
✔ [3945/3973] Built FLT.Mathlib.Data.Fin.Basic (1.1s)
✔ [3946/3973] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.6s)
✔ [3947/3973] Built FLT.Mathlib.GroupTheory.Index (1.1s)
✔ [3948/3973] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.4s)
✔ [3949/3973] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.4s)
✔ [3950/3973] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.4s)
✔ [3951/3973] Built FLT.Mathlib.Topology.Algebra.Monoid (1.3s)
✔ [3952/3973] Built Mathlib.CategoryTheory.Abelian.Transfer (2.1s)
✔ [3953/3973] Built Mathlib.CategoryTheory.Action.Concrete (2.3s)
✔ [3954/3976] Built Mathlib.Analysis.Complex.ExponentialBounds (4.8s)
✔ [3955/3976] Built FLT.Mathlib.Topology.Algebra.Order.Field (3.4s)
✔ [3956/3978] Built Mathlib.Analysis.SumOverResidueClass (1.9s)
✔ [3957/3978] Built Mathlib.CategoryTheory.WithTerminal.Cone (7.3s)
✔ [3958/3980] Built Mathlib.CategoryTheory.Action.Limits (3.5s)
✔ [3959/3983] Built Mathlib.Geometry.Manifold.DerivationBundle (8.4s)
✔ [3960/3983] Built Mathlib.Analysis.Asymptotics.SpecificAsymptotics (2.8s)
✔ [3961/3987] Built Mathlib.Analysis.Real.Pi.Wallis (2.7s)
✔ [3962/3987] Built Mathlib.Data.NNReal.Star (1.3s)
✔ [3963/3987] Built Mathlib.Order.Monotone.Union (1000ms)
✔ [3964/3990] Built Mathlib.CategoryTheory.Subobject.MonoOver (5.3s)
✔ [3965/3990] Built FLT.Patching.Utils.TopologicallyFG (1.8s)
✔ [3966/3990] Built Mathlib.CategoryTheory.Action.Monoidal (6.5s)
✔ [3967/3990] Built Mathlib.Algebra.Ring.Ext (2.3s)
✔ [3968/3992] Built Mathlib.Analysis.PSeries (4.0s)
✔ [3969/3992] Built Mathlib.Data.Real.StarOrdered (1.8s)
✔ [3970/3992] Built Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (1.7s)
✔ [3971/3992] Built Mathlib.CategoryTheory.Subobject.Basic (4.8s)
✔ [3972/3992] Built Mathlib.RepresentationTheory.Action (6.9s)
✔ [3973/3992] Built FLT.Patching.Utils.StructureFiniteness (5.5s)
✔ [3974/3992] Built Mathlib.Analysis.SpecialFunctions.Stirling (5.1s)
✔ [3975/3992] Built Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation (16s)
✔ [3976/3992] Built Mathlib.CategoryTheory.Subobject.WellPowered (1.4s)
✔ [3977/3992] Built Mathlib.CategoryTheory.Subobject.FactorThru (1.7s)
✔ [3978/3995] Built Mathlib.RingTheory.Regular.IsSMulRegular (3.1s)
✔ [3979/3995] Built FLT.NumberField.DiscriminantBounds (4.0s)
✔ [3980/3995] Built Mathlib.CategoryTheory.Subobject.Lattice (5.9s)
✔ [3981/3995] Built Mathlib.Order.GameAdd (1.5s)
✔ [3982/3995] Built Mathlib.CategoryTheory.Simple (2.1s)
✔ [3983/3999] Built FLT.Patching.Ultraproduct (13s)
✔ [3984/3999] Built Mathlib.Data.DFinsupp.WellFounded (2.2s)
✔ [3985/4001] Built Mathlib.RingTheory.Regular.RegularSequence (8.2s)
✔ [3986/4001] Built Mathlib.Algebra.Group.TypeTags.Pointwise (910ms)
✔ [3987/4001] Built Mathlib.Data.Finsupp.WellFounded (1.3s)
✔ [3988/4007] Built Mathlib.CategoryTheory.Preadditive.Schur (2.2s)
✔ [3989/4007] Built Mathlib.Data.Finsupp.Weight (4.0s)
✔ [3990/4009] Built Mathlib.Tactic.MoveAdd (1.7s)
✔ [3992/4016] Built Mathlib.RepresentationTheory.Rep.Basic (30s)
✔ [3993/4016] Built FLT.Patching.Algebra (15s)
✔ [3994/4016] Built Mathlib.RingTheory.MvPowerSeries.Basic (8.9s)
✔ [3995/4016] Built Mathlib.Topology.UniformSpace.Ascoli (2.1s)
✔ [3996/4016] Built Mathlib.Topology.Algebra.Group.SubmonoidClosure (2.0s)
✔ [3997/4016] Built FLT.TateCurve.TateCurve (310ms)
✔ [3998/4016] Built FLT.Patching.Module (19s)
✔ [3999/4016] Built Mathlib.RepresentationTheory.FDRep (5.8s)
✔ [4000/4016] Built FLT.Patching.VanishingFilter (4.1s)
✔ [4001/4016] Built Mathlib.RingTheory.MvPowerSeries.Order (4.1s)
✔ [4002/4016] Built Mathlib.RingTheory.MvPowerSeries.LexOrder (2.6s)
✔ [4003/4016] Built Mathlib.RingTheory.PowerSeries.Basic (5.7s)
✔ [4004/4016] Built Mathlib.Topology.Algebra.Group.CompactOpen (3.5s)
✔ [4005/4016] Built Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (2.5s)
✔ [4006/4016] Built FLT.Patching.Utils.CompactHausdorffRings (3.3s)
✔ [4007/4016] Built Mathlib.RingTheory.KrullDimension.NonZeroDivisors (2.2s)
✔ [4008/4016] Built FLT.Patching.Utils.Depth (4.1s)
✔ [4009/4016] Built FLT.GlobalLanglandsConjectures.GLnDefs (10s)
✔ [4010/4016] Built FLT.Patching.Over (13s)
✔ [4011/4016] Built FLT.GlobalLanglandsConjectures.GLzero (2.1s)
✔ [4012/4016] Built FLT.Patching.System (10s)
✔ [4013/4016] Built FLT.Patching.REqualsT (4.2s)
✔ [4014/4016] Built FLT (1.8s)
✔ [4015/4016] Built FermatsLastTheorem (13s)
Build completed successfully (4016 jobs).

semantic_extract exit 1 duration 10m 49s · created 6/1/2026, 9:13:08 PM

./.apodeixis/tools/lean-semantic-extract.sh

lean semantic helper failed: generated static runner exited non-zero
remediation: inspect the generated repository runner and imported root modules