Login

Verification run

Run 1

promachina/iut-lean branch master triggered via poller
succeeded commit 5fdc2dad5be2 toolchain lean-v4-30-0 prover lean took 1h 54m · finished 6w ago
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 2s · created 
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-13-source
Cloning into '/var/lib/apodeixis/repos/job-13-source'...
git_checkout exit 128 duration 3 ms · created 
git checkout 5fdc2dad5be227c55d5a2039858a6dc680f2e725
fatal: reference is not a tree: 5fdc2dad5be227c55d5a2039858a6dc680f2e725
git_checkout exit 0 duration 752 ms · created 
git fetch --depth 1 origin 5fdc2dad5be227c55d5a2039858a6dc680f2e725
From https://github.com/promachina/iut-lean
 * branch            5fdc2dad5be227c55d5a2039858a6dc680f2e725 -> FETCH_HEAD
git_checkout exit 0 duration 112 ms · created 
git checkout 5fdc2dad5be227c55d5a2039858a6dc680f2e725 (after fetch)
Note: switching to '5fdc2dad5be227c55d5a2039858a6dc680f2e725'.

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 5fdc2da Improve wiki pedagogy
lake_cache exit 1 duration 57s · created 
lake exe cache get
info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision 'c5ea00351c28e24afc9f0f84379aa41082b1188f'
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'
✔ [3/25] Built Cache.Init (405ms)
✔ [4/25] Built Cache.Lean (548ms)
✔ [5/25] Built Cache.Lean:c.o (332ms)
✔ [6/25] Built Cache.Init:c.o (439ms)
✔ [14/25] Built Batteries.Data.String.Basic:c.o (95ms)
✔ [15/25] Built Batteries.Data.Array.Match:c.o (199ms)
✔ [16/25] Built Batteries.Data.String.Matcher:c.o (144ms)
✔ [17/25] Built Cache.IO (1.9s)
✖ [18/25] Building Cache.Hashing (522ms)
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/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
✔ [24/25] Built Cache.IO:c.o (1.2s)
Some required targets logged failures:
- Cache.Hashing
error: build failed
lean_checker exit 0 duration 46m 4s · created 
lake build
Operator.NNNorm (4.0s)
✔ [2453/2505] Built Mathlib.Analysis.Normed.Operator.Asymptotics (2.3s)
✔ [2454/2507] Built Mathlib.Analysis.Complex.Norm (3.3s)
✔ [2455/2507] Built Mathlib.Algebra.Order.Group.Opposite (1.1s)
✔ [2456/2507] Built Mathlib.Algebra.Order.BigOperators.Expect (3.0s)
✔ [2457/2507] Built Mathlib.Analysis.Complex.Order (2.2s)
✔ [2458/2509] Built Mathlib.Algebra.Star.StarProjection (1.7s)
✔ [2459/2509] Built Mathlib.Topology.Algebra.Module.Alternating.Topology (10s)
✔ [2460/2509] Built Mathlib.Algebra.Order.Star.Basic (4.7s)
✔ [2461/2509] Built Mathlib.Analysis.Normed.Operator.Bilinear (17s)
✔ [2462/2509] Built Mathlib.Algebra.Star.Pi (1.3s)
✔ [2463/2514] Built Mathlib.Analysis.Normed.Group.Hom (6.4s)
✔ [2464/2514] Built Mathlib.Analysis.Calculus.FDeriv.Basic (13s)
✔ [2465/2515] Built Mathlib.Algebra.Star.Pointwise (2.2s)
✔ [2466/2515] Built Mathlib.Algebra.Star.Prod (1.3s)
✔ [2467/2515] Built Mathlib.Analysis.Normed.Operator.NormedSpace (7.6s)
✔ [2468/2517] Built Mathlib.Analysis.Calculus.FDeriv.RestrictScalars (3.8s)
✔ [2469/2517] Built Mathlib.Algebra.Star.Center (1.4s)
✔ [2470/2518] Built Mathlib.Analysis.Calculus.FDeriv.Comp (5.0s)
✔ [2471/2518] Built Mathlib.Analysis.Calculus.FDeriv.Congr (4.1s)
✔ [2472/2518] Built Mathlib.Analysis.Normed.Module.Completion (2.7s)
✔ [2473/2520] Built Mathlib.Algebra.Algebra.Spectrum.Basic (4.8s)
✔ [2474/2520] Built Mathlib.Algebra.Star.MonoidHom (2.2s)
✔ [2475/2522] Built Mathlib.Data.Real.Star (1.1s)
✔ [2476/2522] Built Mathlib.Analysis.Normed.Operator.Mul (7.5s)
✔ [2477/2523] Built Mathlib.Analysis.Calculus.FDeriv.Const (4.6s)
✔ [2478/2523] Built Mathlib.Topology.Algebra.Module.Star (2.7s)
✔ [2479/2523] Built Mathlib.Analysis.Normed.Ring.Finite (1.8s)
✔ [2480/2523] Built Mathlib.Analysis.Normed.Module.Multilinear.Basic (26s)
✔ [2481/2527] Built Mathlib.Data.Complex.BigOperators (1.7s)
✔ [2482/2527] Built Mathlib.Algebra.Star.Unitary (5.9s)
✔ [2483/2527] Built Mathlib.Analysis.Calculus.Deriv.Basic (11s)
✔ [2484/2527] Built Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (9.9s)
✔ [2485/2529] Built Mathlib.Algebra.Star.NonUnitalSubalgebra (23s)
✔ [2486/2529] Built Mathlib.Algebra.CharP.Invertible (1.2s)
✔ [2487/2529] Built Mathlib.Topology.Instances.RealVectorSpace (1.8s)
✔ [2488/2529] Built Mathlib.Analysis.Calculus.Deriv.Support (1.7s)
✔ [2489/2529] Built Mathlib.Analysis.Normed.Module.Alternating.Basic (14s)
✔ [2490/2529] Built Mathlib.Analysis.Calculus.FDeriv.Linear (2.9s)
✔ [2491/2529] Built Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle (1.2s)
✔ [2492/2531] Built Mathlib.Analysis.Calculus.Deriv.Comp (9.6s)
✔ [2493/2531] Built Mathlib.Algebra.Star.Subalgebra (11s)
✔ [2494/2533] Built Mathlib.LinearAlgebra.Complex.Module (8.3s)
✔ [2495/2533] Built Mathlib.Analysis.Normed.Module.Multilinear.Curry (18s)
✔ [2496/2533] Built Mathlib.Algebra.CharZero.Infinite (964ms)
✔ [2497/2533] Built Mathlib.SetTheory.Cardinal.Continuum (1.6s)
✔ [2498/2533] Built Mathlib.Analysis.CStarAlgebra.Basic (3.9s)
✔ [2499/2536] Built Mathlib.Data.Rat.Cardinal (1.1s)
✔ [2500/2536] Built Mathlib.Analysis.Calculus.FormalMultilinearSeries (11s)
✔ [2501/2536] Built Mathlib.Analysis.Calculus.FDeriv.Prod (20s)
✔ [2502/2536] Built Mathlib.Analysis.Real.Cardinality (2.3s)
✔ [2503/2536] Built Mathlib.Order.Filter.Subsingleton (1.4s)
✔ [2504/2536] Built Mathlib.Analysis.Calculus.FDeriv.Add (17s)
✔ [2505/2536] Built Mathlib.Order.Filter.EventuallyConst (1.5s)
✔ [2506/2536] Built Mathlib.Analysis.RCLike.Basic (13s)
✔ [2507/2537] Built Mathlib.Analysis.Calculus.FDeriv.Bilinear (4.8s)
✔ [2508/2538] Built Mathlib.Analysis.Calculus.Deriv.Add (6.4s)
✔ [2509/2538] Built Mathlib.Analysis.Analytic.ConvergenceRadius (11s)
✔ [2510/2539] Built Mathlib.Algebra.Field.NegOnePow (1.8s)
✔ [2511/2539] Built Mathlib.Analysis.Complex.Basic (8.4s)
✔ [2512/2539] Built Mathlib.Analysis.Calculus.FDeriv.Equiv (12s)
✔ [2513/2539] Built Mathlib.Algebra.Field.Periodic (1.0s)
✔ [2514/2539] Built Mathlib.Analysis.Calculus.Deriv.Slope (3.6s)
✔ [2515/2540] Built Mathlib.Algebra.QuadraticDiscriminant (2.5s)
✔ [2516/2540] Built Mathlib.Analysis.Analytic.OfScalars (5.3s)
✔ [2517/2540] Built Mathlib.Analysis.Complex.ReImTopology (2.2s)
✔ [2518/2544] Built Mathlib.Analysis.Complex.Asymptotics (1.7s)
✔ [2519/2547] Built Mathlib.Algebra.Order.CauSeq.BigOperators (4.8s)
✔ [2520/2547] Built Mathlib.Analysis.Calculus.FDeriv.CompCLM (21s)
✔ [2521/2547] Built Mathlib.Tactic.NormNum.NatFactorial (2.0s)
✔ [2522/2548] Built Mathlib.Analysis.Complex.Exponential (7.9s)
✔ [2523/2549] Built Mathlib.Topology.Order.AtTopBotIxx (10s)
✔ [2524/2549] Built Mathlib.Analysis.Analytic.Basic (27s)
✔ [2525/2549] Built Mathlib.Analysis.Complex.Trigonometric (6.8s)
✔ [2526/2549] Built Mathlib.Analysis.Normed.Group.Quotient (6.4s)
✔ [2527/2551] Built Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (27s)
✔ [2528/2552] Built Mathlib.Analysis.Normed.Module.Ball.Pointwise (5.1s)
✔ [2529/2554] Built Mathlib.Data.Int.SuccPred (1.2s)
✔ [2530/2554] Built Mathlib.Order.Circular (2.0s)
✔ [2531/2556] Built Mathlib.Analysis.SpecialFunctions.Exp (3.9s)
✔ [2532/2560] Built Mathlib.Algebra.Order.Interval.Set.Group (3.1s)
✔ [2533/2560] Built Mathlib.GroupTheory.QuotientGroup.ModEq (1.9s)
✔ [2534/2561] Built Mathlib.Analysis.Analytic.ChangeOrigin (8.4s)
✔ [2535/2562] Built Mathlib.GroupTheory.Divisible (2.1s)
✔ [2536/2562] Built Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas (1.4s)
✔ [2537/2564] Built Mathlib.Algebra.CharZero.Quotient (2.1s)
✔ [2538/2566] Built Mathlib.Topology.Instances.Sign (1.6s)
✔ [2539/2566] Built Mathlib.Topology.Instances.ZMultiples (1.9s)
✔ [2540/2569] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (8.8s)
✔ [2541/2569] Built Mathlib.Algebra.Order.Ring.Interval (1.6s)
✔ [2542/2576] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (5.3s)
✔ [2543/2576] Built Mathlib.Algebra.Order.ToIntervalMod (14s)
✔ [2544/2580] Built Mathlib.Analysis.Analytic.CPolynomialDef (13s)
✔ [2545/2580] Built Mathlib.Analysis.SpecialFunctions.Log.Basic (5.5s)
✔ [2546/2580] Built Mathlib.Analysis.Calculus.Deriv.Linear (2.1s)
✔ [2547/2580] Built Mathlib.Analysis.Normed.Group.AddTorsor (2.3s)
✔ [2548/2580] Built Mathlib.Topology.Sets.Closeds (3.7s)
✔ [2549/2582] Built Mathlib.Analysis.Analytic.Linear (5.8s)
✔ [2550/2588] Built Mathlib.Topology.Instances.AddCircle.Defs (8.8s)
✔ [2551/2588] Built Mathlib.Analysis.Calculus.Deriv.AffineMap (3.1s)
✔ [2552/2592] Built Mathlib.Topology.LocallyConstant.Basic (3.3s)
✔ [2553/2594] Built Mathlib.Topology.Instances.AddCircle.Real (2.6s)
✔ [2554/2595] Built Mathlib.Topology.OpenPartialHomeomorph.IsImage (2.7s)
✔ [2555/2595] Built Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (4.3s)
✔ [2556/2595] Built Mathlib.Analysis.Analytic.Composition (16s)
✔ [2557/2597] Built Mathlib.Analysis.Calculus.Deriv.Inverse (3.4s)
✔ [2558/2600] Built Mathlib.Analysis.Normed.Group.AddCircle (3.9s)
✔ [2559/2600] Built Mathlib.Topology.Algebra.ContinuousAffineMap (9.9s)
✔ [2560/2600] Built Mathlib.Algebra.Algebra.TransferInstance (1.4s)
✔ [2561/2600] Built Mathlib.Topology.MetricSpace.CauSeqFilter (1.9s)
✔ [2562/2600] Built Mathlib.Analysis.Calculus.FDeriv.Affine (3.3s)
✔ [2563/2601] Built Mathlib.Analysis.Analytic.Inverse (13s)
✔ [2564/2601] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (11s)
✔ [2565/2607] Built Mathlib.Analysis.Calculus.LocalExtr.Basic (4.2s)
✔ [2566/2607] Built Mathlib.Analysis.Normed.Algebra.Exponential (9.5s)
✔ [2567/2611] Built Mathlib.Topology.ExtendFrom (1.6s)
✔ [2568/2611] Built Mathlib.Analysis.Normed.Group.Lemmas (1.8s)
✔ [2569/2611] Built Mathlib.Analysis.SpecialFunctions.Complex.Arg (5.9s)
✔ [2570/2611] Built Mathlib.Topology.Order.ExtendFrom (1.4s)
✔ [2571/2613] Built Mathlib.Topology.Algebra.AffineSubspace (1.5s)
✔ [2572/2613] Built Mathlib.Topology.Order.Rolle (1.8s)
✔ [2573/2614] Built Mathlib.Analysis.SpecialFunctions.Complex.Log (3.0s)
✔ [2574/2615] Built Mathlib.Topology.Algebra.ContinuousAffineEquiv (5.3s)
✔ [2575/2615] Built Mathlib.Analysis.Calculus.LocalExtr.Rolle (1.6s)
✔ [2576/2615] Built Mathlib.Analysis.Normed.Module.RCLike.Basic (2.8s)
✔ [2577/2615] Built Mathlib.Topology.Algebra.Module.Determinant (1.9s)
✔ [2578/2615] Built Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (2.3s)
✔ [2579/2616] Built Mathlib.Analysis.Normed.Module.RieszLemma (2.8s)
✔ [2580/2617] Built Mathlib.Order.Atoms.Finite (1.6s)
✔ [2581/2622] Built Mathlib.Analysis.Analytic.Constructions (30s)
✔ [2582/2622] Built Mathlib.Topology.Algebra.Module.ModuleTopology (5.2s)
✔ [2583/2622] Built Mathlib.Order.CompactlyGenerated.Intervals (1.4s)
✔ [2584/2622] Built Mathlib.Analysis.Analytic.Within (2.9s)
✔ [2585/2625] Built Mathlib.Analysis.Analytic.Uniqueness (3.7s)
✔ [2586/2626] Built Mathlib.Control.Bifunctor (1.5s)
✔ [2587/2626] Built Mathlib.Analysis.Normed.Affine.Isometry (12s)
✔ [2588/2626] Built Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient (1.6s)
✔ [2589/2629] Built Mathlib.Logic.Equiv.Functor (1.0s)
✔ [2590/2630] Built Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional (1.3s)
✔ [2591/2632] Built Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent (4.6s)
✔ [2592/2632] Built Mathlib.Topology.Homeomorph.Quotient (1.2s)
✔ [2593/2632] Built Mathlib.Order.JordanHolder (3.5s)
✔ [2594/2632] Built Mathlib.Topology.Instances.Matrix (3.2s)
✔ [2595/2632] Built Mathlib.Analysis.Analytic.CPolynomial (11s)
✔ [2596/2632] Built Mathlib.Topology.Maps.Strict.Basic (1.6s)
✔ [2597/2634] Built Mathlib.LinearAlgebra.Dimension.LinearMap (2.6s)
✔ [2598/2634] Built Mathlib.Topology.Algebra.Module.Complement (5.3s)
✔ [2599/2638] Built Mathlib.Data.Finset.Update (1.6s)
✔ [2600/2642] Built Mathlib.Tactic.Measurability.Init (798ms)
✔ [2601/2642] Built Mathlib.Data.Prod.TProd (1.8s)
✔ [2602/2648] Built Mathlib.GroupTheory.GroupAction.IterateAct (795ms)
✔ [2603/2652] Built Mathlib.Tactic.Measurability (1.0s)
✔ [2604/2656] Built Mathlib.MeasureTheory.OuterMeasure.Defs (1.7s)
✔ [2605/2660] Built Mathlib.MeasureTheory.MeasurableSpace.Defs (2.9s)
✔ [2606/2667] Built Mathlib.Data.Set.Dissipate (1.6s)
✔ [2607/2667] Built Mathlib.RingTheory.SimpleModule.Basic (8.1s)
✔ [2608/2667] Built Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable (1.5s)
✔ [2609/2667] Built Mathlib.MeasureTheory.OuterMeasure.Basic (2.6s)
✔ [2610/2667] Built Mathlib.MeasureTheory.MeasurableSpace.Instances (1.8s)
✔ [2611/2667] Built Mathlib.MeasureTheory.MeasurableSpace.Basic (2.2s)
✔ [2612/2668] Built Mathlib.Order.Interval.Set.Monotone (1.9s)
✔ [2613/2668] Built Mathlib.Topology.Algebra.Module.Simple (1.7s)
✔ [2614/2668] Built Mathlib.MeasureTheory.PiSystem (3.3s)
✔ [2615/2668] Built Mathlib.MeasureTheory.OuterMeasure.AE (3.8s)
✔ [2616/2672] Built Mathlib.MeasureTheory.OuterMeasure.Operations (4.1s)
✔ [2617/2672] Built Mathlib.Data.Set.MemPartition (2.4s)
✔ [2618/2672] Built Mathlib.MeasureTheory.MeasurableSpace.Constructions (5.2s)
✔ [2619/2676] Built Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (1.8s)
✔ [2620/2676] Built Mathlib.Order.Filter.CountableSeparatingOn (1.9s)
✔ [2621/2676] Built Mathlib.Analysis.Calculus.FDeriv.Analytic (21s)
✔ [2622/2676] Built Mathlib.MeasureTheory.OuterMeasure.OfFunction (3.3s)
✔ [2623/2676] Built Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (2.4s)
✔ [2624/2676] Built Mathlib.Topology.Separation.GDelta (1.4s)
✔ [2625/2676] Built Mathlib.MeasureTheory.MeasurableSpace.Embedding (5.6s)
✔ [2626/2676] Built Mathlib.Topology.Algebra.Module.FiniteDimension (14s)
✔ [2627/2676] Built Mathlib.Analysis.SpecialFunctions.Exponential (6.4s)
✔ [2628/2676] Built Mathlib.MeasureTheory.OuterMeasure.Caratheodory (2.6s)
✔ [2629/2676] Built Mathlib.Topology.GDelta.MetrizableSpace (1.6s)
✔ [2630/2676] Built Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (2.7s)
✔ [2631/2676] Built Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (22s)
✔ [2632/2677] Built Mathlib.Analysis.Calculus.ContDiff.Defs (23s)
✔ [2633/2680] Built Mathlib.MeasureTheory.OuterMeasure.Induced (3.4s)
✔ [2634/2680] Built Mathlib.MeasureTheory.Measure.MeasureSpaceDef (4.1s)
✔ [2635/2681] Built Mathlib.MeasureTheory.Function.AEMeasurableSequence (1.9s)
✔ [2636/2683] Built Mathlib.Analysis.Normed.Module.FiniteDimension (10s)
✔ [2637/2683] Built Mathlib.MeasureTheory.Measure.AEDisjoint (1.9s)
✔ [2638/2687] Built Mathlib.MeasureTheory.MeasurableSpace.Prod (1.7s)
✔ [2639/2693] Built Mathlib.Analysis.Calculus.ContDiff.Basic (13s)
✔ [2640/2693] Built Mathlib.MeasureTheory.Measure.NullMeasurable (2.0s)
✔ [2641/2693] Built Mathlib.Topology.Metrizable.Real (1.8s)
✔ [2642/2693] Built Mathlib.Algebra.Order.Monoid.Canonical.Basic (5.1s)
✔ [2643/2695] Built Mathlib.Topology.IndicatorConstPointwise (1.8s)
✔ [2644/2695] Built Mathlib.Analysis.Calculus.FDeriv.Mul (35s)
✔ [2645/2695] Built Mathlib.Topology.Instances.Real.Lemmas (2.6s)
✔ [2646/2695] Built Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (2.9s)
✔ [2647/2695] Built Mathlib.Analysis.Calculus.DSlope (3.4s)
✔ [2648/2695] Built Mathlib.Analysis.Calculus.DiffContOnCl (3.7s)
✔ [2649/2697] Built Mathlib.MeasureTheory.Measure.MeasureSpace (8.3s)
✔ [2650/2697] Built Mathlib.Analysis.Calculus.ContDiff.Comp (12s)
✔ [2651/2697] Built Mathlib.Analysis.LocallyConvex.Polar (4.2s)
✔ [2652/2697] Built Mathlib.Analysis.Calculus.FDeriv.Pow (7.9s)
✔ [2653/2699] Built Mathlib.MeasureTheory.Measure.Map (2.9s)
✔ [2654/2701] Built Mathlib.Analysis.Analytic.IsolatedZeros (6.8s)
✔ [2655/2701] Built Mathlib.Analysis.Calculus.ContDiff.Deriv (3.4s)
✔ [2656/2701] Built Mathlib.Geometry.Convex.Cone.Basic (6.0s)
✔ [2657/2701] Built Mathlib.Analysis.Calculus.Deriv.Pow (3.7s)
✔ [2658/2703] Built Mathlib.Analysis.Calculus.Deriv.Mul (17s)
✔ [2659/2703] Built Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (2.3s)
✔ [2660/2703] Built Mathlib.Analysis.RCLike.Lemmas (2.0s)
✔ [2661/2703] Built Mathlib.Analysis.Calculus.IteratedDeriv.Defs (4.5s)
✔ [2662/2703] Built Mathlib.Analysis.RCLike.Extend (5.7s)
✔ [2663/2703] Built Mathlib.Analysis.Convex.Cone.Extension (2.8s)
✔ [2664/2703] Built Mathlib.Analysis.Calculus.Deriv.CompMul (1.0s)
✔ [2665/2703] Built Mathlib.Analysis.Calculus.Deriv.MeanValue (3.9s)
✔ [2666/2703] Built Mathlib.Analysis.Calculus.Deriv.Polynomial (3.6s)
✔ [2667/2703] Built Mathlib.Analysis.Calculus.Deriv.Inv (4.4s)
✔ [2668/2703] Built Mathlib.Analysis.Calculus.MeanValue (8.5s)
✔ [2669/2703] Built Mathlib.Analysis.Convex.TotallyBounded (1.7s)
✔ [2670/2705] Built Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (2.5s)
✔ [2671/2705] Built Mathlib.Analysis.Calculus.Deriv.Shift (2.3s)
✔ [2672/2705] Built Mathlib.Analysis.Normed.Module.RCLike.Extend (2.4s)
✔ [2673/2705] Built Mathlib.Analysis.LocallyConvex.AbsConvex (3.6s)
✔ [2674/2705] Built Mathlib.MeasureTheory.Measure.Comap (2.4s)
✔ [2675/2709] Built Mathlib.Analysis.Calculus.ContDiff.Operations (27s)
✔ [2676/2709] Built Mathlib.Algebra.Central.Defs (1.3s)
✔ [2677/2709] Built Mathlib.Analysis.Calculus.ContDiff.RCLike (3.9s)
✔ [2678/2709] Built Mathlib.Algebra.Central.Basic (2.3s)
✔ [2679/2709] Built Mathlib.Analysis.Calculus.Deriv.ZPow (4.0s)
✔ [2680/2709] Built Mathlib.Analysis.Normed.Module.HahnBanach (5.0s)
✔ [2681/2709] Built Mathlib.Analysis.Complex.RealDeriv (3.5s)
✔ [2682/2710] Built Mathlib.MeasureTheory.Measure.Restrict (7.2s)
✔ [2683/2710] Built Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms (1.9s)
✔ [2684/2710] Built Mathlib.Analysis.Calculus.LogDeriv (4.7s)
✔ [2685/2710] Built Mathlib.Analysis.Convex.Gauge (7.1s)
✔ [2686/2710] Built Mathlib.MeasureTheory.Measure.Typeclasses.Finite (4.3s)
✔ [2687/2723] Built Mathlib.Combinatorics.Enumerative.InclusionExclusion (4.2s)
✔ [2688/2724] Built Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (5.6s)
✔ [2689/2724] Built Mathlib.MeasureTheory.Measure.MutuallySingular (3.9s)
✔ [2690/2724] Built Mathlib.Analysis.LocallyConvex.Separation (7.9s)
✔ [2691/2724] Built Mathlib.MeasureTheory.Measure.Typeclasses.Probability (2.6s)
✔ [2692/2725] Built Mathlib.MeasureTheory.Measure.Trim (2.0s)
✔ [2693/2725] Built Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (2.4s)
✔ [2694/2725] Built Mathlib.MeasureTheory.Measure.AEMeasurable (3.2s)
✔ [2695/2725] Built Mathlib.MeasureTheory.Measure.Dirac (3.7s)
✔ [2696/2725] Built Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (24s)
✔ [2697/2725] Built Mathlib.MeasureTheory.Group.Defs (1.7s)
✔ [2698/2725] Built Mathlib.MeasureTheory.Measure.Count (1.8s)
✔ [2699/2725] Built Mathlib.Analysis.LocallyConvex.SeparatingDual (6.4s)
✔ [2700/2725] Built Mathlib.MeasureTheory.Order.Lattice (1.9s)
✔ [2701/2727] Built Mathlib.Dynamics.Ergodic.MeasurePreserving (2.1s)
✔ [2702/2730] Built Mathlib.Analysis.Normed.Group.FunctionSeries (2.6s)
✔ [2703/2732] Built Mathlib.Analysis.Normed.Module.Dual (3.0s)
✔ [2704/2735] Built Mathlib.Analysis.SpecialFunctions.ExpDeriv (4.6s)
✔ [2705/2736] Built Mathlib.MeasureTheory.Group.Arithmetic (6.8s)
✔ [2706/2736] Built Mathlib.Topology.MetricSpace.Gluing (3.7s)
✔ [2707/2739] Built Mathlib.Topology.Separation.CountableSeparatingOn (1.7s)
✔ [2708/2739] Built Mathlib.Topology.Metrizable.CompletelyMetrizable (2.7s)
✔ [2709/2739] Built Mathlib.Topology.MetricSpace.PiNat (7.1s)
✔ [2710/2739] Built Mathlib.MeasureTheory.Measure.Doubling (2.1s)
✔ [2711/2740] Built Mathlib.Topology.MetricSpace.CantorScheme (1.8s)
✔ [2712/2742] Built Mathlib.Analysis.SpecialFunctions.Log.Deriv (8.7s)
✔ [2713/2744] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (5.6s)
✔ [2714/2745] Built Mathlib.Dynamics.Minimal (1.7s)
✔ [2715/2745] Built Mathlib.Topology.MetricSpace.Polish (2.4s)
✔ [2716/2745] Built Mathlib.MeasureTheory.Measure.OpenPos (2.3s)
✔ [2717/2745] Built Mathlib.MeasureTheory.Group.MeasurableEquiv (4.6s)
✔ [2718/2745] Built Mathlib.GroupTheory.Complement (7.2s)
✔ [2719/2748] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (2.0s)
✔ [2720/2748] Built Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap (2.8s)
✔ [2721/2752] Built Mathlib.MeasureTheory.Group.Pointwise (1.7s)
✔ [2722/2752] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Order (6.6s)
✔ [2723/2752] Built Mathlib.Topology.MetricSpace.Perfect (2.1s)
✔ [2724/2754] Built Mathlib.Topology.ContinuousMap.CocompactMap (1.5s)
✔ [2725/2756] Built Mathlib.MeasureTheory.Measure.Regular (4.7s)
✔ [2726/2761] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Real (4.7s)
✔ [2727/2761] Built Mathlib.Data.Nat.NthRoot.Defs (838ms)
✔ [2728/2761] Built Mathlib.Analysis.SpecialFunctions.Pow.Complex (3.7s)
✔ [2729/2761] Built Mathlib.Tactic.Qify (1.1s)
✔ [2730/2761] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (1.8s)
✔ [2731/2761] Built Mathlib.Tactic.Rify (1.5s)
✔ [2732/2762] Built Mathlib.MeasureTheory.Group.Action (4.0s)
✔ [2733/2762] Built Mathlib.MeasureTheory.Function.SimpleFunc (10s)
✔ [2734/2766] Built Mathlib.Analysis.SpecialFunctions.Pow.Real (7.6s)
✔ [2735/2766] Built Mathlib.MeasureTheory.Constructions.Polish.Basic (5.0s)
✔ [2736/2766] Built Mathlib.Order.Filter.Germ.Basic (5.5s)
✔ [2737/2767] Built Mathlib.MeasureTheory.Integral.Lebesgue.Basic (5.7s)
✔ [2738/2767] Built Mathlib.MeasureTheory.Function.SimpleFuncDense (2.8s)
✔ [2739/2767] Built Mathlib.Topology.Compactness.CompactlyCoherentSpace (2.1s)
✔ [2740/2767] Built Mathlib.MeasureTheory.Integral.Lebesgue.Norm (1.9s)
✔ [2741/2768] Built Mathlib.Order.Filter.ENNReal (3.5s)
✔ [2742/2768] Built Mathlib.MeasureTheory.Integral.Lebesgue.Add (5.1s)
✔ [2743/2773] Built Mathlib.Analysis.SpecialFunctions.Pow.NNReal (8.0s)
✔ [2744/2773] Built Mathlib.Topology.UniformSpace.CompactConvergence (3.1s)
✔ [2745/2773] Built Mathlib.Probability.ConditionalProbability (2.9s)
✔ [2746/2773] Built Mathlib.MeasureTheory.Integral.Lebesgue.Map (2.1s)
✔ [2747/2773] Built Mathlib.MeasureTheory.Integral.Lebesgue.Sub (2.5s)
✔ [2748/2777] Built Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (8.2s)
✔ [2749/2777] Built Mathlib.MeasureTheory.Integral.Lebesgue.Markov (2.4s)
✔ [2750/2777] Built Mathlib.MeasureTheory.MeasurableSpace.Pi (1.8s)
✔ [2751/2777] Built Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (3.3s)
✔ [2752/2778] Built Mathlib.MeasureTheory.Integral.Lebesgue.Countable (3.1s)
✔ [2753/2778] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Complex (1.8s)
✔ [2754/2778] Built Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (2.1s)
✔ [2755/2778] Built Mathlib.MeasureTheory.Function.Egorov (2.3s)
✔ [2756/2778] Built Mathlib.MeasureTheory.Measure.GiryMonad (2.8s)
✔ [2757/2780] Built Mathlib.Topology.ContinuousMap.Algebra (8.6s)
✔ [2758/2780] Built Mathlib.Analysis.SpecialFunctions.Pow.Continuity (5.3s)
✔ [2759/2782] Built Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (6.3s)
✔ [2760/2782] Built Mathlib.Data.ENNReal.Holder (1.5s)
✔ [2761/2782] Built Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (2.2s)
✔ [2762/2783] Built Mathlib.Analysis.Normed.Group.Indicator (1.5s)
✔ [2763/2787] Built Mathlib.Algebra.BigOperators.Field (1.8s)
✔ [2764/2787] Built Mathlib.MeasureTheory.Function.AEEqFun (6.8s)
✔ [2765/2787] Built Mathlib.MeasureTheory.Measure.Prod (8.1s)
✔ [2766/2787] Built Mathlib.Analysis.Convex.Slope (6.1s)
✔ [2767/2793] Built Mathlib.Data.Real.ConjExponents (4.3s)
✔ [2768/2798] Built Mathlib.MeasureTheory.Group.Convolution (3.6s)
✔ [2769/2805] Built Mathlib.Analysis.Calculus.FDeriv.Measurable (12s)
✔ [2770/2805] Built Mathlib.Analysis.Convex.SpecificFunctions.Basic (3.5s)
✔ [2771/2805] Built Mathlib.Order.Monotone.Monovary (1.6s)
✔ [2772/2805] Built Mathlib.Order.Filter.IndicatorFunction (1.4s)
✔ [2773/2813] Built Mathlib.MeasureTheory.Measure.Real (3.6s)
✔ [2774/2813] Built Mathlib.MeasureTheory.Group.Measure (10s)
✔ [2775/2813] Built Mathlib.Algebra.Order.Monovary (5.6s)
✔ [2776/2813] Built Mathlib.Analysis.MeanInequalities (8.7s)
✔ [2777/2814] Built Mathlib.MeasureTheory.Group.LIntegral (2.5s)
✔ [2778/2814] Built Mathlib.MeasureTheory.Constructions.Pi (7.7s)
✔ [2779/2815] Built Mathlib.Algebra.Module.MinimalAxioms (824ms)
✔ [2780/2818] Built Mathlib.Analysis.Normed.Operator.Extend (9.9s)
✔ [2781/2820] Built Mathlib.Probability.UniformOn (2.5s)
✔ [2782/2820] Built Mathlib.MeasureTheory.Group.Prod (5.2s)
✔ [2783/2820] Built Mathlib.Topology.Algebra.Indicator (1.6s)
✔ [2784/2820] Built Mathlib.Analysis.Convex.Mul (5.9s)
✔ [2785/2824] Built Mathlib.Topology.Bornology.BoundedOperation (2.2s)
✔ [2786/2827] Built Mathlib.Topology.ContinuousMap.Star (2.2s)
✔ [2787/2827] Built Mathlib.MeasureTheory.Function.EssSup (2.9s)
✔ [2788/2828] Built Mathlib.Analysis.LConvolution (3.1s)
✔ [2789/2828] Built Mathlib.Topology.NoetherianSpace (2.3s)
✔ [2790/2829] Built Mathlib.Analysis.MeanInequalitiesPow (3.2s)
✔ [2791/2829] Built Mathlib.MeasureTheory.Function.LpSeminorm.Defs (1.0s)
✔ [2792/2829] Built Mathlib.Topology.QuasiSeparated (2.4s)
✔ [2793/2829] Built Mathlib.Topology.ContinuousMap.Bounded.Basic (7.5s)
✔ [2794/2829] Built Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (3.0s)
✔ [2795/2830] Built Mathlib.MeasureTheory.Measure.WithDensity (5.9s)
✔ [2796/2830] Built Mathlib.MeasureTheory.Integral.MeanInequalities (4.3s)
✔ [2797/2832] Built Mathlib.Topology.MetricSpace.ThickenedIndicator (3.5s)
✔ [2798/2832] Built Mathlib.Topology.Sets.Compacts (4.2s)
✔ [2799/2832] Built Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (2.9s)
✔ [2800/2833] Built Mathlib.MeasureTheory.Function.LpSeminorm.Basic (8.2s)
✔ [2801/2833] Built Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (4.6s)
✔ [2802/2833] Built Mathlib.Analysis.Normed.Operator.CompleteCodomain (3.1s)
✔ [2803/2833] Built Mathlib.Topology.ContinuousMap.Bounded.Normed (9.4s)
✔ [2804/2834] Built Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (2.6s)
✔ [2805/2834] Built Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (3.2s)
✔ [2806/2834] Built Mathlib.LinearAlgebra.Matrix.Diagonal (2.2s)
✔ [2807/2836] Built Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (2.5s)
✔ [2808/2836] Built Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (2.8s)
✔ [2809/2836] Built Mathlib.Topology.ContinuousMap.Bounded.Star (2.6s)
✔ [2810/2839] Built Mathlib.MeasureTheory.Integral.Marginal (3.4s)
✔ [2811/2839] Built Mathlib.MeasureTheory.Function.LpSeminorm.SMul (3.3s)
✔ [2812/2839] Built Mathlib.Topology.Order.LeftRightLim (3.1s)
✔ [2813/2839] Built Mathlib.Topology.Algebra.Group.Compact (1.3s)
✔ [2814/2839] Built Mathlib.MeasureTheory.Measure.Content (3.7s)
✔ [2815/2839] Built Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (4.9s)
✔ [2816/2842] Built Mathlib.Topology.ContinuousMap.Compact (7.4s)
✔ [2817/2842] Built Mathlib.MeasureTheory.Measure.Stieltjes (6.2s)
✔ [2818/2848] Built Mathlib.MeasureTheory.Measure.Haar.Basic (5.9s)
✔ [2819/2852] Built Mathlib.Topology.Baire.CompleteMetrizable (1.8s)
✔ [2820/2853] Built Mathlib.Analysis.InnerProductSpace.Defs (6.5s)
✔ [2821/2853] Built Mathlib.Topology.ContinuousMap.ContinuousMapZero (7.7s)
✔ [2822/2856] Built Mathlib.Topology.Algebra.Module.ClosedSubmodule (5.4s)
✔ [2823/2856] Built Mathlib.MeasureTheory.Function.LpSpace.Basic (18s)
✔ [2824/2856] Built Mathlib.Algebra.DirectSum.Decomposition (4.1s)
✔ [2825/2860] Built Mathlib.Analysis.Normed.Operator.Banach (13s)
✔ [2826/2860] Built Mathlib.Analysis.InnerProductSpace.Basic (11s)
✔ [2827/2860] Built Mathlib.MeasureTheory.Function.LpSpace.Complete (3.6s)
✔ [2828/2862] Built Mathlib.MeasureTheory.Function.LpSpace.Indicator (4.1s)
✔ [2829/2866] Built Mathlib.Analysis.InnerProductSpace.Continuous (3.0s)
✔ [2830/2868] Built Mathlib.Analysis.Normed.Lp.WithLp (3.4s)
✔ [2831/2868] Built Mathlib.MeasureTheory.Function.ConvergenceInMeasure (3.6s)
✔ [2832/2870] Built Mathlib.Data.Matrix.Reflection (2.6s)
✔ [2833/2870] Built Mathlib.Analysis.InnerProductSpace.Projection.Minimal (4.0s)
✔ [2834/2873] Built Mathlib.Util.Superscript (1.8s)
✔ [2835/2873] Built Mathlib.MeasureTheory.Topology (1.4s)
✔ [2836/2873] Built Mathlib.MeasureTheory.Function.LpOrder (2.7s)
✔ [2837/2873] Built Mathlib.Topology.Algebra.IsUniformGroup.Order (1.7s)
✔ [2838/2874] Built Mathlib.LinearAlgebra.UnitaryGroup (4.6s)
✔ [2839/2880] Built Mathlib.Analysis.Calculus.TangentCone.Prod (2.2s)
✔ [2840/2880] Built Mathlib.Order.Filter.AtTopBot.Floor (1.7s)
✔ [2841/2880] Built Mathlib.Analysis.InnerProductSpace.LinearMap (12s)
✔ [2842/2880] Built Mathlib.Analysis.Normed.Lp.ProdLp (12s)
✔ [2843/2880] Built Mathlib.Topology.Algebra.Order.Floor (2.7s)
✔ [2844/2887] Built Mathlib.Analysis.BoxIntegral.Box.Basic (3.5s)
✔ [2845/2887] Built Mathlib.Analysis.InnerProductSpace.Orthonormal (5.8s)
✔ [2846/2889] Built Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (2.5s)
✔ [2847/2892] Built Mathlib.MeasureTheory.Function.L1Space.Integrable (12s)
✔ [2848/2893] Built Mathlib.Analysis.BoxIntegral.Partition.Basic (3.0s)
✔ [2849/2893] Built Mathlib.Analysis.InnerProductSpace.Subspace (4.4s)
✔ [2850/2896] Built Mathlib.MeasureTheory.Function.L1Space.AEEqFun (3.8s)
✔ [2851/2896] Built Mathlib.Analysis.Oscillation (2.3s)
✔ [2852/2896] Built Mathlib.Analysis.BoxIntegral.Partition.Split (2.7s)
✔ [2853/2896] Built Mathlib.MeasureTheory.Integral.IntegrableOn (6.2s)
✔ [2854/2896] Built Mathlib.Analysis.Normed.Lp.PiLp (15s)
✔ [2855/2896] Built Mathlib.Analysis.BoxIntegral.Partition.Tagged (3.1s)
✔ [2856/2896] Built Mathlib.MeasureTheory.Function.LpSeminorm.Prod (1.9s)
✔ [2857/2896] Built Mathlib.Analysis.BoxIntegral.Partition.Additive (3.1s)
✔ [2858/2896] Built Mathlib.Analysis.InnerProductSpace.Orthogonal (8.4s)
✔ [2859/2896] Built Mathlib.Analysis.Normed.Lp.Matrix (4.6s)
✔ [2860/2900] Built Mathlib.MeasureTheory.Function.LocallyIntegrable (6.9s)
✔ [2861/2904] Built Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (2.2s)
✔ [2862/2906] Built Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (10s)
✔ [2863/2906] Built Mathlib.Analysis.BoxIntegral.Partition.Filter (3.1s)
✔ [2864/2908] Built Mathlib.Analysis.Normed.Lp.MeasurableSpace (2.2s)
✔ [2865/2908] Built Mathlib.LinearAlgebra.Orientation (5.2s)
✔ [2866/2910] Built Mathlib.Analysis.InnerProductSpace.Symmetric (5.5s)
✔ [2867/2914] Built Mathlib.Analysis.Complex.Cardinality (1.0s)
✔ [2868/2914] Built Mathlib.FieldTheory.PolynomialGaloisGroup (4.6s)
✔ [2869/2914] Built Mathlib.LinearAlgebra.Complex.FiniteDimensional (3.2s)
✔ [2870/2914] Built Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (3.9s)
✔ [2871/2915] Built Mathlib.MeasureTheory.Integral.FinMeasAdditive (8.1s)
✔ [2872/2915] Built Mathlib.Topology.Maps.Proper.CompactlyGenerated (2.2s)
✔ [2873/2916] Built Mathlib.RingTheory.Polynomial.Vieta (2.6s)
✔ [2874/2916] Built Mathlib.RingTheory.Finiteness.Quotient (1.9s)
✔ [2875/2919] Built Mathlib.Analysis.InnerProductSpace.Projection.Basic (10s)
✔ [2876/2919] Built Mathlib.Topology.Algebra.Polynomial (2.8s)
✔ [2877/2919] Built Mathlib.Algebra.CharP.Quotient (1.5s)
✔ [2878/2920] Built Mathlib.Algebra.Field.ZMod (1.2s)
✔ [2879/2920] Built Mathlib.Data.ZMod.ValMinAbs (2.2s)
✔ [2880/2921] Built Mathlib.Analysis.InnerProductSpace.Projection.Submodule (4.4s)
✔ [2881/2923] Built Mathlib.Analysis.InnerProductSpace.Projection.Reflection (4.1s)
✔ [2882/2923] Built Mathlib.LinearAlgebra.FreeModule.Determinant (1.4s)
✔ [2883/2923] Built Mathlib.Data.Int.Associated (1.0s)
✔ [2884/2923] Built Mathlib.Data.Int.NatAbs (1.1s)
✔ [2885/2925] Built Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (3.4s)
✔ [2886/2927] Built Mathlib.FieldTheory.Finite.Basic (6.3s)
✔ [2887/2928] Built Mathlib.Data.SetLike.Fintype (1.7s)
✔ [2888/2932] Built Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (8.1s)
✔ [2889/2932] Built Mathlib.RingTheory.Artinian.Defs (1.6s)
✔ [2890/2933] Built Mathlib.RingTheory.Ideal.Quotient.PowTransition (3.9s)
✔ [2891/2933] Built Mathlib.RingTheory.Jacobson.Semiprimary (1.8s)
✔ [2892/2933] Built Mathlib.RingTheory.Spectrum.Maximal.Basic (1.4s)
✔ [2893/2933] Built Mathlib.RingTheory.LocalRing.RingHom.Basic (2.2s)
✔ [2894/2933] Built Mathlib.RingTheory.Artinian.Module (6.5s)
✔ [2895/2935] Built Mathlib.MeasureTheory.Integral.SetToL1 (30s)
✔ [2896/2939] Built Mathlib.RingTheory.FiniteLength (2.4s)
✔ [2897/2939] Built Mathlib.Algebra.GroupWithZero.Submonoid.Instances (1.3s)
✔ [2898/2939] Built Mathlib.RingTheory.AdicCompletion.Basic (15s)
✔ [2899/2943] Built Mathlib.RingTheory.Length (4.4s)
✔ [2900/2943] Built Mathlib.Algebra.Order.GroupWithZero.WithZero (1.7s)
✔ [2901/2947] Built Mathlib.RingTheory.Bezout (1.5s)
✔ [2902/2949] Built Mathlib.Algebra.GroupWithZero.Range (3.2s)
✔ [2903/2949] Built Mathlib.GroupTheory.PGroup (3.3s)
✔ [2904/2949] Built Mathlib.Algebra.Order.GroupWithZero.Range (2.3s)
✔ [2905/2949] Built Mathlib.MeasureTheory.Integral.Bochner.L1 (11s)
✔ [2906/2951] Built Mathlib.RingTheory.Coprime.Ideal (1.0s)
✔ [2907/2951] Built Mathlib.Analysis.InnerProductSpace.PiL2 (26s)
✔ [2908/2952] Built Mathlib.GroupTheory.Torsion (3.4s)
✔ [2909/2954] Built Mathlib.GroupTheory.Sylow (5.3s)
✔ [2910/2954] Built Mathlib.Analysis.InnerProductSpace.ProdL2 (5.9s)
✔ [2911/2954] Built Mathlib.Algebra.Polynomial.Module.AEval (8.4s)
✔ [2912/2954] Built Mathlib.MeasureTheory.Integral.Bochner.Basic (13s)
✔ [2913/2954] Built Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (5.8s)
✔ [2914/2954] Built Mathlib.RingTheory.Valuation.Basic (15s)
✔ [2915/2956] Built Mathlib.RingTheory.Finiteness.Nakayama (2.2s)
✔ [2916/2956] Built Mathlib.RingTheory.ReesAlgebra (1.8s)
✔ [2917/2956] Built Mathlib.Algebra.Module.ZMod (2.1s)
✔ [2918/2956] Built Mathlib.MeasureTheory.Measure.Haar.OfBasis (7.8s)
✔ [2919/2958] Built Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (3.0s)
✔ [2920/2958] Built Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (4.0s)
✔ [2921/2958] Built Mathlib.Analysis.InnerProductSpace.Orientation (5.3s)
✔ [2922/2958] Built Mathlib.RingTheory.Valuation.PrimeMultiplicity (2.1s)
✔ [2923/2958] Built Mathlib.Algebra.Polynomial.Module.Basic (7.2s)
✔ [2924/2958] Built Mathlib.RingTheory.LocalRing.ResidueField.Defs (1.6s)
✔ [2925/2958] Built Mathlib.RingTheory.Valuation.Integers (5.5s)
✔ [2926/2958] Built Mathlib.MeasureTheory.Measure.Lebesgue.Basic (6.3s)
✔ [2927/2958] Built Mathlib.RingTheory.Nakayama (4.0s)
✔ [2928/2958] Built Mathlib.RingTheory.LocalRing.ResidueField.Basic (3.6s)
✔ [2929/2958] Built Mathlib.Algebra.Module.Torsion.Basic (11s)
✔ [2930/2958] Built Mathlib.RingTheory.Filtration (5.5s)
✔ [2931/2960] Built Mathlib.MeasureTheory.Integral.Bochner.Set (11s)
✔ [2932/2960] Built Mathlib.Analysis.BoxIntegral.Partition.Measure (1.0s)
✔ [2933/2960] Built Mathlib.RingTheory.Valuation.ValuationRing (4.5s)
✔ [2934/2960] Built Mathlib.RingTheory.Ideal.Cotangent (8.0s)
✔ [2935/2960] Built Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (10s)
✔ [2936/2962] Built Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (7.5s)
✔ [2937/2962] Built Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus (1.9s)
✔ [2938/2962] Built Mathlib.RingTheory.Jacobson.Polynomial (1.6s)
✔ [2939/2962] Built Mathlib.RingTheory.DiscreteValuationRing.Basic (4.1s)
✔ [2940/2962] Built Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (6.9s)
✔ [2941/2963] Built Mathlib.Algebra.Order.Ring.Idempotent (2.7s)
✔ [2942/2963] Built Mathlib.Analysis.BoxIntegral.Basic (11s)
✔ [2943/2963] Built Mathlib.MeasureTheory.Group.FundamentalDomain (21s)
✔ [2944/2963] Built Mathlib.Order.Heyting.Hom (3.4s)
✔ [2945/2964] Built Mathlib.MeasureTheory.Measure.Lebesgue.Complex (3.3s)
✔ [2946/2964] Built Mathlib.RingTheory.Ideal.MinimalPrime.Localization (3.9s)
✔ [2947/2964] Built Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (14s)
✔ [2948/2964] Built Mathlib.RingTheory.Jacobson.Ring (8.2s)
✔ [2949/2968] Built Mathlib.Analysis.BoxIntegral.Integrability (5.0s)
✔ [2950/2969] Built Mathlib.RingTheory.Localization.AsSubring (2.4s)
✔ [2951/2972] Built Mathlib.Analysis.BoxIntegral.DivergenceTheorem (4.4s)
✔ [2952/2973] Built Mathlib.Topology.Sets.OpenCover (2.5s)
✔ [2953/2973] Built Mathlib.RingTheory.SurjectiveOnStalks (4.8s)
✔ [2954/2976] Built Mathlib.MeasureTheory.Integral.DominatedConvergence (6.9s)
✔ [2955/2976] Built Mathlib.Topology.LocallyClosed (1.8s)
✔ [2956/2976] Built Mathlib.Topology.Spectral.Hom (1.6s)
✔ [2957/2976] Built Mathlib.Order.BooleanSubalgebra (7.8s)
✔ [2958/2976] Built Mathlib.RingTheory.LocalRing.ResidueField.Ideal (5.4s)
✔ [2959/2976] Built Mathlib.MeasureTheory.Measure.Haar.Quotient (6.6s)
✔ [2960/2982] Built Mathlib.Order.Ideal (3.7s)
✔ [2961/2982] Built Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (9.7s)
✔ [2962/2982] Built Mathlib.MeasureTheory.Integral.Prod (7.3s)
✔ [2963/2982] Built Mathlib.Topology.LocalAtTarget (3.8s)
✔ [2964/2982] Built Mathlib.Topology.Spectral.Prespectral (2.1s)
✔ [2965/2982] Built Mathlib.Topology.Sober (1.8s)
✔ [2966/2982] Built Mathlib.RingTheory.Spectrum.Prime.RingHom (4.2s)
✔ [2967/2984] Built Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (5.8s)
✔ [2968/2984] Built Mathlib.Analysis.SpecialFunctions.NonIntegrable (3.8s)
✔ [2969/2984] Built Mathlib.Topology.Spectral.Basic (1.2s)
✔ [2970/2984] Built Mathlib.Topology.Constructible (3.9s)
✔ [2971/2984] Built Mathlib.Topology.KrullDimension (1.3s)
✔ [2972/2984] Built Mathlib.MeasureTheory.Integral.DivergenceTheorem (7.4s)
✔ [2973/2985] Built Mathlib.RingTheory.Localization.Submodule (2.7s)
✔ [2974/2989] Built Mathlib.CategoryTheory.Category.Init (745ms)
✔ [2975/2998] Built Mathlib.RingTheory.Spectrum.Maximal.Localization (3.8s)
✔ [2976/2998] Built Mathlib.RingTheory.LocalProperties.Submodule (3.6s)
✔ [2977/3003] Built Mathlib.Data.Opposite (676ms)
✔ [2978/3005] Built Mathlib.Tactic.CategoryTheory.CategoryStar (517ms)
✔ [2979/3007] Built Mathlib.Combinatorics.Quiver.Basic (928ms)
✔ [2980/3007] Built Mathlib.Logic.Lemmas (1.1s)
✔ [2981/3010] Built Mathlib.Combinatorics.Quiver.Prefunctor (1.1s)
✔ [2982/3010] Built Mathlib.Combinatorics.Quiver.Push (1.1s)
✔ [2983/3010] Built Mathlib.CategoryTheory.Category.Basic (3.4s)
✔ [2984/3010] Built Mathlib.Combinatorics.Quiver.Path (2.7s)
✔ [2985/3010] Built Mathlib.MeasureTheory.Integral.CircleIntegral (8.2s)
✔ [2986/3010] Built Mathlib.CategoryTheory.Functor.Basic (2.1s)
✔ [2987/3016] Built Mathlib.Combinatorics.Quiver.Symmetric (1.2s)
✔ [2988/3018] Built Mathlib.Tactic.CategoryTheory.Reassoc (1.5s)
✔ [2989/3018] Built Mathlib.RingTheory.Spectrum.Prime.Topology (8.8s)
✔ [2990/3018] Built Mathlib.Tactic.CategoryTheory.Slice (1.3s)
✔ [2991/3047] Built Mathlib.CategoryTheory.NatTrans (1.9s)
✔ [2992/3047] Built Mathlib.RingTheory.KrullDimension.Zero (2.3s)
✔ [2993/3049] Built Mathlib.CategoryTheory.ConcreteCategory.Bundled (558ms)
✔ [2994/3108] Built Mathlib.CategoryTheory.Iso (3.6s)
✔ [2995/3108] Built Mathlib.Analysis.Complex.CauchyIntegral (5.7s)
✔ [2996/3108] Built Mathlib.Algebra.Ring.Shrink (1.4s)
✔ [2997/3108] Built Mathlib.Tactic.CategoryTheory.IsoReassoc (1.1s)
✔ [2998/3112] Built Mathlib.CategoryTheory.ObjectProperty.Basic (1.5s)
✔ [2999/3129] Built Mathlib.RingTheory.DiscreteValuationRing.TFAE (3.4s)
✔ [3000/3146] Built Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (1.2s)
✔ [3001/3146] Built Mathlib.CategoryTheory.Functor.Category (3.2s)
✔ [3002/3146] Built Mathlib.CategoryTheory.HomCongr (1.2s)
✔ [3003/3149] Built Mathlib.CategoryTheory.Thin (1.6s)
✔ [3004/3149] Built Mathlib.Analysis.Complex.Liouville (3.5s)
✔ [3005/3155] Built Mathlib.RingTheory.ChainOfDivisors (2.8s)
✔ [3006/3156] Built Mathlib.Algebra.Ring.Subsemiring.Pointwise (1.8s)
✔ [3007/3156] Built Mathlib.CategoryTheory.NatIso (3.6s)
✔ [3008/3159] Built Mathlib.Analysis.Complex.Polynomial.Basic (3.5s)
✔ [3009/3159] Built Mathlib.RingTheory.Ideal.Basis (2.0s)
✔ [3010/3159] Built Mathlib.Algebra.Ring.Subring.Pointwise (2.2s)
✔ [3011/3159] Built Mathlib.RingTheory.FractionalIdeal.Basic (6.1s)
✔ [3012/3162] Built Mathlib.CategoryTheory.Functor.FullyFaithful (2.8s)
✔ [3013/3162] Built Mathlib.RingTheory.Norm.Basic (3.4s)
✔ [3014/3164] Built Mathlib.Algebra.Algebra.Subalgebra.Pointwise (1.7s)
✔ [3015/3164] Built Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (1.8s)
✔ [3016/3164] Built Mathlib.CategoryTheory.Bicategory.Basic (6.0s)
✔ [3017/3164] Built Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (4.2s)
✔ [3018/3164] Built Mathlib.CategoryTheory.InducedCategory (1.5s)
✔ [3019/3164] Built Mathlib.Algebra.GroupWithZero.Torsion (1.6s)
✔ [3020/3168] Built Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp (1.5s)
✔ [3021/3168] Built Mathlib.CategoryTheory.ObjectProperty.FullSubcategory (1.8s)
✔ [3022/3168] Built Mathlib.Order.Interval.Finset.DenselyOrdered (1.6s)
✔ [3023/3168] Built Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (4.8s)
✔ [3024/3169] Built Mathlib.CategoryTheory.EssentialImage (1.8s)
✔ [3025/3169] Built Mathlib.CategoryTheory.Whiskering (9.0s)
✔ [3026/3170] Built Mathlib.CategoryTheory.ConcreteCategory.Basic (1.6s)
✔ [3027/3170] Built Mathlib.RingTheory.FractionalIdeal.Operations (10s)
✔ [3028/3171] Built Mathlib.Algebra.Order.Group.Cyclic (1.7s)
✔ [3029/3171] Built Mathlib.CategoryTheory.Functor.ReflectsIso.Basic (1.1s)
✔ [3030/3172] Built Mathlib.Tactic.CategoryTheory.Elementwise (1.4s)
✔ [3031/3172] Built Mathlib.Algebra.Order.Ring.IsNonarchimedean (2.5s)
✔ [3032/3172] Built Mathlib.RingTheory.FractionalIdeal.Inverse (3.7s)
✔ [3033/3172] Built Mathlib.Data.Int.WithZero (2.1s)
✔ [3034/3173] Built Mathlib.GroupTheory.ArchimedeanDensely (7.7s)
✔ [3035/3174] Built Mathlib.CategoryTheory.Elementwise (1.0s)
✔ [3036/3174] Built Mathlib.CategoryTheory.Equivalence (6.6s)
✔ [3037/3174] Built Mathlib.RingTheory.Valuation.ExtendToLocalization (1.8s)
✔ [3038/3174] Built Mathlib.Algebra.Field.TransferInstance (1.1s)
✔ [3039/3178] Built Mathlib.RingTheory.Valuation.Archimedean (2.9s)
✔ [3040/3180] Built Mathlib.RingTheory.DedekindDomain.Ideal.Basic (6.4s)
✔ [3041/3184] Built Mathlib.Topology.Algebra.OpenSubgroup (4.4s)
✔ [3042/3184] Built Mathlib.Topology.Algebra.UniformFilterBasis (1.6s)
✔ [3043/3184] Built Mathlib.CategoryTheory.Opposites (7.0s)
✔ [3044/3184] Built Mathlib.Topology.Algebra.Nonarchimedean.Basic (2.6s)
✔ [3045/3187] Built Mathlib.RingTheory.Valuation.ValuativeRel.Basic (10s)
✔ [3046/3187] Built Mathlib.Topology.Algebra.WithZeroTopology (2.6s)
✔ [3047/3187] Built Mathlib.CategoryTheory.Functor.TwoSquare (3.1s)
✔ [3048/3187] Built Mathlib.CategoryTheory.Functor.Const (1.9s)
✔ [3049/3187] Built Mathlib.CategoryTheory.EqToHom (2.3s)
✔ [3050/3190] Built Mathlib.RingTheory.Valuation.ValuationSubring (9.3s)
✔ [3051/3190] Built Mathlib.Topology.Algebra.Nonarchimedean.Bases (2.5s)
✔ [3052/3190] Built Mathlib.RingTheory.Ideal.Oka (1.4s)
✔ [3053/3190] Built Mathlib.CategoryTheory.Bicategory.Strict.Basic (1.1s)
✔ [3054/3190] Built Mathlib.CategoryTheory.Category.ULift (1.8s)
✔ [3055/3190] Built Mathlib.CategoryTheory.Category.Preorder (1.8s)
✔ [3056/3190] Built Mathlib.CategoryTheory.Products.Basic (4.5s)
✔ [3057/3194] Built Mathlib.RingTheory.PrincipalIdealDomainOfPrime (2.1s)
✔ [3058/3194] Built Mathlib.Data.Real.Embedding (4.1s)
✔ [3059/3194] Built Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (18s)
✔ [3060/3194] Built Mathlib.CategoryTheory.Functor.Currying (4.4s)
✔ [3061/3194] Built Mathlib.CategoryTheory.Pi.Basic (4.8s)
✔ [3062/3195] Built Mathlib.Topology.Algebra.Valued.ValuationTopology (8.2s)
✔ [3063/3195] Built Mathlib.Topology.MetricSpace.Ultra.Basic (1.8s)
✔ [3064/3195] Built Mathlib.RingTheory.Valuation.RankOne (5.2s)
✔ [3065/3199] Built Mathlib.Analysis.Normed.Field.TransferInstance (1.4s)
✔ [3066/3199] Built Mathlib.CategoryTheory.Discrete.Basic (2.9s)
✔ [3067/3199] Built Mathlib.CategoryTheory.Products.Unitor (1.1s)
✔ [3068/3199] Built Mathlib.Analysis.Normed.Ring.TransferInstance (1.3s)
✔ [3069/3199] Built Mathlib.CategoryTheory.FinCategory.Basic (1.1s)
✔ [3070/3204] Built Mathlib.Analysis.Normed.Group.Ultra (3.2s)
✔ [3071/3204] Built Mathlib.CategoryTheory.PUnit (1.4s)
✔ [3072/3204] Built Mathlib.CategoryTheory.PEmpty (985ms)
✔ [3073/3204] Built Mathlib.CategoryTheory.FinCategory.AsType (1.4s)
✔ [3074/3204] Built Mathlib.Analysis.Normed.Ring.WithAbs (3.4s)
✔ [3075/3206] Built Mathlib.Topology.Algebra.Valued.NormedValued (5.3s)
✔ [3076/3206] Built Mathlib.RingTheory.Norm.Transitivity (5.2s)
✔ [3077/3206] Built Mathlib.CategoryTheory.Comma.Basic (10s)
✔ [3078/3206] Built Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (5.2s)
✔ [3079/3206] Built Mathlib.Topology.Instances.Complex (2.0s)
✔ [3080/3208] Built Mathlib.Analysis.Normed.Field.WithAbs (4.5s)
✔ [3081/3208] Built Mathlib.Topology.Algebra.Valued.ValuedField (19s)
✔ [3082/3210] Built Mathlib.CategoryTheory.Comma.Arrow (3.4s)
✔ [3083/3210] Built Mathlib.Tactic.Algebra.Lemmas (2.2s)
✔ [3084/3210] Built Mathlib.RingTheory.Discriminant (4.2s)
✔ [3085/3211] Built Mathlib.CategoryTheory.CommSq (3.1s)
✔ [3086/3211] Built Mathlib.Tactic.ArithMult.Init (722ms)
✔ [3087/3212] Built Mathlib.Analysis.AbsoluteValue.Equivalence (7.4s)
✔ [3088/3212] Built Mathlib.CategoryTheory.MorphismProperty.Basic (4.6s)
✔ [3089/3213] Built Mathlib.Tactic.CancelDenoms (1.2s)
✔ [3090/3213] Built Mathlib.Tactic.ArithMult (853ms)
✔ [3091/3213] Built Mathlib.RingTheory.Localization.NormTrace (3.0s)
✔ [3092/3213] Built Mathlib.Tactic.Cases (1.5s)
✔ [3093/3213] Built Mathlib.Tactic.Algebra.Basic (5.1s)
✔ [3094/3213] Built Mathlib.CategoryTheory.Groupoid (2.1s)
✔ [3095/3213] Built Mathlib.Tactic.CategoryTheory.BicategoricalComp (1.5s)
✔ [3096/3213] Built Mathlib.CategoryTheory.MorphismProperty.Composition (2.3s)
✔ [3097/3213] Built Mathlib.Topology.Algebra.Valued.WithVal (11s)
✔ [3098/3213] Built Mathlib.CategoryTheory.MorphismProperty.Factorization (2.6s)
✔ [3099/3217] Built Mathlib.CategoryTheory.Endomorphism (1.7s)
✔ [3100/3224] Built Mathlib.CategoryTheory.IsConnected (1.0s)
✔ [3101/3229] Built Mathlib.NumberTheory.NumberField.Norm (2.7s)
✔ [3102/3230] Built Mathlib.CategoryTheory.EpiMono (1.9s)
✔ [3103/3230] Built Mathlib.Tactic.CategoryTheory.Coherence.Datatypes (1.3s)
✔ [3104/3230] Built Mathlib.CategoryTheory.Bicategory.Functor.Prelax (1.9s)
✔ [3105/3230] Built Mathlib.Tactic.CategoryTheory.CancelIso (1.2s)
✔ [3106/3230] Built Mathlib.CategoryTheory.Retract (1.8s)
✔ [3107/3230] Built Mathlib.CategoryTheory.Balanced (1.2s)
✔ [3108/3230] Built Mathlib.CategoryTheory.Types.Basic (2.7s)
✔ [3109/3230] Built Mathlib.Tactic.CategoryTheory.CheckCompositions (1.5s)
✔ [3110/3230] Built Mathlib.CategoryTheory.Monad.Basic (3.0s)
✔ [3111/3230] Built Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (6.2s)
✔ [3112/3230] Built Mathlib.CategoryTheory.LiftingProperties.Basic (1.7s)
✔ [3113/3230] Built Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence (4.8s)
✔ [3114/3230] Built Mathlib.Tactic.CategoryTheory.Coherence.Normalize (3.8s)
✔ [3115/3230] Built Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes (3.7s)
✔ [3116/3230] Built Mathlib.CategoryTheory.Functor.Hom (1.1s)
✔ [3117/3234] Built Mathlib.CategoryTheory.ConcreteCategory.Forget (1.6s)
✔ [3118/3234] Built Mathlib.CategoryTheory.Limits.Types.ColimitType (2.1s)
✔ [3119/3234] Built Mathlib.CategoryTheory.Category.Cat (3.5s)
✔ [3120/3234] Built Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (1.4s)
✔ [3121/3234] Built Mathlib.Tactic.CategoryTheory.Coherence.Basic (1.5s)
✔ [3122/3236] Built Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso (1.1s)
✔ [3123/3236] Built Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence (3.0s)
✔ [3124/3236] Built Mathlib.Tactic.CategoryTheory.Bicategory.Normalize (3.4s)
✔ [3125/3236] Built Mathlib.Tactic.CategoryTheory.ToApp (1.8s)
✔ [3126/3236] Built Mathlib.CategoryTheory.Functor.Trifunctor (3.3s)
✔ [3127/3236] Built Mathlib.Algebra.Category.MonCat.Basic (4.3s)
✔ [3128/3236] Built Mathlib.CategoryTheory.Category.Cat.AsSmall (1.3s)
✔ [3129/3238] Built Mathlib.CategoryTheory.IsomorphismClasses (1.1s)
✔ [3130/3238] Built Mathlib.Tactic.CategoryTheory.Bicategory.Basic (3.3s)
✔ [3131/3238] Built Mathlib.CategoryTheory.Bicategory.Functor.Oplax (4.3s)
✔ [3132/3241] Built Mathlib.CategoryTheory.Bicategory.Functor.Lax (4.7s)
✔ [3133/3242] Built Mathlib.CategoryTheory.Yoneda (11s)
✔ [3134/3243] Built Mathlib.Tactic.Change (586ms)
✔ [3135/3243] Built Mathlib.Algebra.Category.MonCat.ForgetCorepresentable (1.3s)
✔ [3136/3243] Built Mathlib.Algebra.Category.Grp.Basic (5.3s)
✔ [3137/3243] Built Mathlib.CategoryTheory.Monoidal.Category (8.5s)
✔ [3138/3244] Built Mathlib.Tactic.Clean (556ms)
✔ [3139/3244] Built Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor (7.9s)
✔ [3140/3244] Built Mathlib.Tactic.ComputeAsymptotics.Lemmas (1.7s)
✔ [3141/3244] Built Mathlib.Tactic.CategoryTheory.MonoidalComp (1.4s)
✔ [3142/3244] Built Mathlib.CategoryTheory.Adjunction.Basic (6.3s)
✔ [3143/3244] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (2.0s)
✔ [3144/3246] Built Mathlib.Algebra.Category.Ring.Basic (5.3s)
✔ [3145/3246] Built Mathlib.CategoryTheory.Limits.Cones (12s)
✔ [3146/3246] Built Mathlib.CategoryTheory.LiftingProperties.Adjunction (1.7s)
✔ [3147/3246] Built Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes (3.5s)
✔ [3148/3246] Built Mathlib.CategoryTheory.Bicategory.Free (6.0s)
✔ [3149/3246] Built Mathlib.CategoryTheory.Adjunction.FullyFaithful (2.4s)
✔ [3150/3248] Built Mathlib.CategoryTheory.Skeletal (2.7s)
✔ [3151/3248] Built Mathlib.Order.CompleteLattice.Group (1.2s)
✔ [3152/3248] Built Mathlib.Algebra.Category.Ring.Instances (2.1s)
✔ [3153/3248] Built Mathlib.CategoryTheory.Functor.EpiMono (2.2s)
✔ [3154/3248] Built Mathlib.CategoryTheory.Adjunction.Mates (5.0s)
✔ [3155/3248] Built Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (3.4s)
✔ [3156/3248] Built Mathlib.Tactic.CategoryTheory.BicategoryCoherence (1.9s)
✔ [3157/3248] Built Mathlib.CategoryTheory.EssentiallySmall (1.9s)
✔ [3158/3248] Built Mathlib.Tactic.CategoryTheory.Monoidal.Normalize (4.4s)
✔ [3159/3248] Built Mathlib.Dynamics.FixedPoints.Topology (1.2s)
✔ [3160/3248] Built Mathlib.CategoryTheory.Limits.IsLimit (9.6s)
✔ [3161/3248] Built Mathlib.CategoryTheory.Monad.Algebra (4.1s)
✔ [3162/3248] Built Mathlib.Topology.MetricSpace.UniformConvergence (5.2s)
✔ [3163/3252] Built Mathlib.CategoryTheory.ShrinkYoneda (3.6s)
✔ [3164/3252] Built Mathlib.Topology.MetricSpace.Contracting (2.3s)
✔ [3165/3254] Built Mathlib.Tactic.CategoryTheory.Monoidal.Basic (3.3s)
✔ [3166/3254] Built Mathlib.Data.Stream.Defs (953ms)
✔ [3167/3254] Built Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (3.9s)
✔ [3168/3257] Built Mathlib.Tactic.ENatToNat (1.5s)
✔ [3169/3257] Built Mathlib.CategoryTheory.Monoidal.Functor (13s)
✔ [3170/3259] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (2.3s)
✔ [3171/3260] Built Mathlib.Data.Stream.Init (2.0s)
✔ [3172/3261] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates (1.5s)
✔ [3173/3261] Built Mathlib.CategoryTheory.Limits.HasLimits (7.9s)
✔ [3174/3261] Built Mathlib.CategoryTheory.Monoidal.Free.Basic (3.7s)
✔ [3175/3261] Built Mathlib.Tactic.DeriveCountable (2.3s)
✔ [3176/3261] Built Mathlib.Data.Seq.Computation (3.7s)
✔ [3177/3263] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (2.4s)
✔ [3178/3263] Built Mathlib.Tactic.DeriveEncodable (3.2s)
✔ [3179/3263] Built Mathlib.CategoryTheory.Limits.Shapes.Terminal (2.0s)
✔ [3180/3263] Built Mathlib.CategoryTheory.Limits.Types.Colimits (1.9s)
✔ [3181/3263] Built Mathlib.Algebra.Category.Ring.Colimits (4.1s)
✔ [3182/3263] Built Mathlib.CategoryTheory.Limits.Types.Limits (2.3s)
✔ [3183/3263] Built Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (14s)
✔ [3184/3264] Built Mathlib.CategoryTheory.Limits.Preserves.Basic (3.1s)
✔ [3185/3264] Built Mathlib.Tactic.CategoryTheory.Coherence (2.7s)
✔ [3186/3264] Built Mathlib.Control.Traversable.Lemmas (940ms)
✔ [3187/3264] Built Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (6.7s)
✔ [3188/3264] Built Mathlib.Data.Seq.Defs (2.7s)
✔ [3189/3264] Built Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (1.8s)
✔ [3190/3264] Built Mathlib.CategoryTheory.Limits.Types.Yoneda (3.6s)
✔ [3191/3264] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal (1.6s)
✔ [3192/3264] Built Mathlib.CategoryTheory.Elements (5.5s)
✔ [3193/3264] Built Mathlib.CategoryTheory.Limits.Shapes.Products (12s)
✔ [3194/3265] Built Mathlib.Tactic.Eval (511ms)
✔ [3195/3265] Built Mathlib.CategoryTheory.Limits.Preserves.Limits (1.8s)
✔ [3196/3265] Built Mathlib.CategoryTheory.Limits.Creates (3.5s)
✔ [3197/3265] Built Mathlib.Tactic.DeriveTraversable (2.7s)
✔ [3198/3267] Built Mathlib.CategoryTheory.EffectiveEpi.Basic (2.4s)
✔ [3199/3268] Built Mathlib.Data.Seq.Basic (4.7s)
✔ [3200/3268] Built Mathlib.Tactic.Explode.Datatypes (755ms)
✔ [3201/3268] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (4.4s)
✔ [3202/3269] Built Mathlib.CategoryTheory.Limits.Preserves.Ulift (1.3s)
✔ [3203/3269] Built Mathlib.Algebra.Category.MonCat.Limits (5.2s)
✔ [3204/3270] Built Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (5.8s)
✔ [3205/3270] Built Mathlib.Tactic.Ext (475ms)
✔ [3206/3271] Built Mathlib.Tactic.Explode.Pretty (788ms)
✔ [3207/3271] Built Mathlib.Tactic.FindSyntax (888ms)
✔ [3208/3272] Built Mathlib.Tactic.Generalize (520ms)
✔ [3209/3272] Built Mathlib.Tactic.Explode (993ms)
✔ [3210/3274] Built Mathlib.CategoryTheory.Limits.Yoneda (2.1s)
✔ [3211/3274] Built Mathlib.Tactic.GeneralizeProofs (456ms)
✔ [3212/3274] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (6.8s)
✔ [3213/3278] Built Mathlib.Tactic.Have (819ms)
✔ [3215/3279] Built Mathlib.Tactic.Linarith.NNRealPreprocessor (1.4s)
✔ [3216/3279] Built Mathlib.CategoryTheory.Comma.Over.Basic (21s)
✔ [3217/3280] Built Mathlib.Tactic.Linter.CommandRanges (584ms)
✔ [3218/3280] Built Mathlib.Tactic.ITauto (2.5s)
✔ [3219/3280] Built Mathlib.Tactic.Linter.CommandStart (498ms)
✔ [3220/3280] Built Mathlib.Tactic.LinearCombinationPrime (2.3s)
✔ [3221/3285] Built Mathlib.Tactic.Linarith.Oracle.FourierMotzkin (1.6s)
✔ [3224/3287] Built Mathlib.Tactic.Linter.FindDeprecations (1.3s)
✔ [3226/3287] Built Mathlib.Tactic.Linter.TextBased.UnicodeLinter (1.1s)
✔ [3227/3288] Built Mathlib.Tactic.Linter.ValidatePRTitle (1.0s)
✔ [3228/3290] Built Mathlib.Tactic.ModCases (1.6s)
✔ [3229/3291] Built Mathlib.Tactic.Monotonicity.Basic (745ms)
✔ [3230/3292] Built Mathlib.Tactic.Monotonicity.Lemmas (851ms)
✔ [3231/3292] Built Mathlib.Tactic.Linter.TextBased (2.5s)
✔ [3232/3292] Built Mathlib.Tactic.Monotonicity (917ms)
✔ [3233/3296] Built Mathlib.Tactic.MoveAdd (1.5s)
✔ [3234/3297] Built Mathlib.CategoryTheory.Grothendieck (7.7s)
✔ [3235/3297] Built Mathlib.Data.Rat.Sqrt (1.1s)
✔ [3236/3297] Built Mathlib.Tactic.NormNum.IsCoprime (1.5s)
✔ [3237/3297] Built Mathlib.Tactic.NormNum.BigOperators (3.3s)
✔ [3238/3297] Built Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (10s)
✔ [3239/3297] Built Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (3.4s)
✔ [3240/3297] Built Mathlib.Tactic.NormNum.IsSquare (3.3s)
✔ [3241/3297] Built Mathlib.NumberTheory.Real.Irrational (2.0s)
✔ [3242/3302] Built Mathlib.CategoryTheory.Limits.Types.Products (2.2s)
✔ [3243/3302] Built Mathlib.CategoryTheory.Monad.Products (2.6s)
✔ [3244/3302] Built Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (1.6s)
✔ [3245/3304] Built Mathlib.Data.Int.Range (985ms)
✔ [3246/3304] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (3.4s)
✔ [3247/3304] Built Mathlib.Data.Nat.Factorization.PrimePow (1.7s)
✔ [3248/3308] Built Mathlib.Tactic.NormNum.Irrational (3.0s)
✔ [3249/3308] Built Mathlib.Data.PNat.Prime (1.6s)
✔ [3250/3308] Built Mathlib.NumberTheory.MulChar.Basic (3.9s)
✔ [3251/3316] Built Mathlib.RingTheory.Valuation.IsTrivialOn (2.2s)
✔ [3252/3316] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (3.6s)
✔ [3253/3316] Built Mathlib.FieldTheory.RatFunc.Defs (2.4s)
✔ [3254/3316] Built Mathlib.NumberTheory.LegendreSymbol.ZModChar (2.2s)
✔ [3255/3316] Built Mathlib.RingTheory.UniqueFactorizationDomain.Nat (1.2s)
✔ [3256/3321] Built Mathlib.RingTheory.RootsOfUnity.Complex (2.6s)
✔ [3257/3321] Built Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (2.6s)
✔ [3258/3321] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (5.3s)
✔ [3259/3322] Built Mathlib.Data.Nat.Squarefree (3.0s)
✔ [3260/3322] Built Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (2.6s)
✔ [3261/3322] Built Mathlib.NumberTheory.LegendreSymbol.Basic (2.5s)
✔ [3262/3322] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (2.1s)
✔ [3263/3323] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (5.3s)
✔ [3264/3327] Built Mathlib.CategoryTheory.Limits.Shapes.Equalizers (8.7s)
✔ [3265/3327] Built Mathlib.NumberTheory.ArithmeticFunction.Defs (6.4s)
✔ [3266/3327] Built Mathlib.RingTheory.Polynomial.Eisenstein.Basic (2.0s)
✔ [3267/3327] Built Mathlib.FieldTheory.KrullTopology (6.1s)
✔ [3268/3327] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (3.5s)
✔ [3269/3328] Built Mathlib.FieldTheory.RatFunc.Basic (20s)
✔ [3270/3328] Built Mathlib.CategoryTheory.Limits.Connected (1.8s)
✔ [3271/3328] Built Mathlib.FieldTheory.Galois.GaloisClosure (3.2s)
✔ [3272/3328] Built Mathlib.CategoryTheory.Comma.Over.Pullback (5.9s)
✔ [3273/3328] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (5.4s)
✔ [3274/3328] Built Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (1.5s)
✔ [3275/3328] Built Mathlib.Topology.Algebra.Group.ClosedSubgroup (1.6s)
✔ [3276/3329] Built Mathlib.Algebra.GCDMonoid.IntegrallyClosed (1.8s)
✔ [3277/3329] Built Mathlib.NumberTheory.ArithmeticFunction.Zeta (2.1s)
✔ [3278/3329] Built Mathlib.RingTheory.Adjoin.PowerBasis (4.1s)
✔ [3279/3329] Built Mathlib.CategoryTheory.Limits.Opposites (4.1s)
✔ [3280/3329] Built Mathlib.CategoryTheory.Filtered.Basic (4.1s)
✔ [3281/3329] Built Mathlib.CategoryTheory.Limits.Shapes.Images (5.5s)
✔ [3282/3329] Built Mathlib.RingTheory.RootsOfUnity.Minpoly (3.4s)
✔ [3283/3329] Built Mathlib.NumberTheory.Padics.PadicVal.Basic (3.6s)
✔ [3284/3329] Built Mathlib.NumberTheory.ArithmeticFunction.Misc (3.0s)
✔ [3285/3329] Built Mathlib.FieldTheory.Galois.Infinite (5.7s)
✔ [3286/3329] Built Mathlib.CategoryTheory.Filtered.Connected (1.3s)
✔ [3287/3329] Built Mathlib.CategoryTheory.Limits.Types.Filtered (2.4s)
✔ [3288/3335] Built Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (4.9s)
✔ [3289/3335] Built Mathlib.CategoryTheory.Limits.Types.Images (1.5s)
✔ [3290/3335] Built Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (4.1s)
✔ [3291/3335] Built Mathlib.FieldTheory.Galois.Abelian (2.3s)
✔ [3292/3335] Built Mathlib.NumberTheory.ArithmeticFunction.Moebius (2.9s)
✔ [3293/3335] Built Mathlib.CategoryTheory.Limits.Final (8.8s)
✔ [3294/3335] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs (2.7s)
✔ [3295/3338] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (3.4s)
✔ [3296/3338] Built Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers (4.1s)
✔ [3297/3338] Built Mathlib.Analysis.Normed.Module.Ray (2.1s)
✔ [3298/3338] Built Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic (1.7s)
✔ [3299/3342] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (1.8s)
✔ [3300/3342] Built Mathlib.Algebra.Algebra.ZMod (1.4s)
✔ [3301/3343] Built Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (2.0s)
✔ [3302/3349] Built Mathlib.Data.ZMod.Units (2.0s)
✔ [3303/3349] Built Mathlib.Analysis.Convex.StrictConvexSpace (2.9s)
✔ [3304/3349] Built Mathlib.CategoryTheory.Limits.Shapes.RegularMono (3.8s)
✔ [3305/3350] Built Mathlib.Algebra.CharP.CharAndCard (1.7s)
✔ [3306/3350] Built Mathlib.FieldTheory.Finite.GaloisField (4.2s)
✔ [3307/3350] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (4.0s)
✔ [3308/3352] Built Mathlib.NumberTheory.MulChar.Lemmas (3.2s)
✔ [3309/3352] Built Mathlib.Tactic.NormNum.ModEq (1.3s)
✔ [3310/3353] Built Mathlib.Analysis.Convex.Uniform (2.5s)
✔ [3311/3354] Built Mathlib.FieldTheory.Finite.Trace (1.7s)
✔ [3312/3354] Built Mathlib.CategoryTheory.Limits.Shapes.KernelPair (1.9s)
✔ [3313/3355] Built Mathlib.CategoryTheory.Limits.Shapes.Kernels (10s)
✔ [3314/3356] Built Mathlib.Data.Nat.Fib.Basic (2.0s)
✔ [3315/3356] Built Mathlib.Tactic.NormNum.NatSqrt (1.3s)
✔ [3316/3357] Built Mathlib.Analysis.InnerProductSpace.Convex (1.7s)
✔ [3317/3357] Built Mathlib.Tactic.NormNum.NatLog (1.4s)
✔ [3318/3357] Built Mathlib.Tactic.NormNum.NatFib (1.4s)
✔ [3319/3358] Built Mathlib.Tactic.NormNum.Ordinal (2.3s)
✔ [3320/3358] Built Mathlib.Tactic.NormNum.Parity (1.4s)
✔ [3321/3359] Built Mathlib.CategoryTheory.Preadditive.Basic (3.2s)
✔ [3322/3360] Built Mathlib.Analysis.Complex.Arg (1.7s)
✔ [3323/3360] Built Mathlib.Tactic.NormNum.PowMod (1.4s)
✔ [3324/3361] Built Mathlib.Tactic.NormNum.Prime (1.7s)
✔ [3325/3362] Built Mathlib.Algebra.Category.Grp.Preadditive (1.9s)
✔ [3326/3363] Built Mathlib.Tactic.PNatToNat (1.6s)
✔ [3327/3363] Built Mathlib.Tactic.Polyrith (621ms)
✔ [3328/3364] Built Mathlib.Tactic.NormNum.RealSqrt (2.4s)
✔ [3329/3364] Built Mathlib.Tactic.Propose (440ms)
✔ [3330/3364] Built Mathlib.CategoryTheory.Limits.Shapes.Diagonal (7.5s)
✔ [3331/3367] Built Mathlib.Tactic.ProdAssoc (875ms)
✔ [3332/3368] Built Mathlib.Tactic.ReduceModChar.Ext (476ms)
✔ [3333/3369] Built Mathlib.Algebra.Category.Grp.ForgetCorepresentable (1.5s)
✔ [3334/3369] Built Mathlib.Tactic.Recall (971ms)
✔ [3335/3370] Built Mathlib.Tactic.Relation.Symm (535ms)
✔ [3336/3370] Built Mathlib.Tactic.Replace (574ms)
✔ [3337/3370] Built Mathlib.Tactic.RewriteSearch (570ms)
✔ [3338/3375] Built Mathlib.Tactic.Ring.NamePolyVars (1.6s)
✔ [3339/3376] Built Mathlib.Tactic.ReduceModChar (2.9s)
✔ [3340/3377] Built Mathlib.Algebra.Group.TypeTags.Pointwise (1.0s)
✔ [3341/3378] Built Mathlib.CategoryTheory.MorphismProperty.Limits (4.0s)
✔ [3342/3378] Built Mathlib.Tactic.Sat.FromLRAT (1.0s)
✔ [3343/3379] Built Mathlib.Tactic.SetNotationForOrder (1.3s)
✔ [3344/3380] Built Mathlib.Tactic.Simproc.Divisors (1.3s)
✔ [3345/3381] Built Mathlib.Tactic.Simproc.Factors (1.8s)
✔ [3346/3381] Built Mathlib.Algebra.Category.Grp.Limits (7.0s)
✔ [3347/3381] Built Mathlib.Tactic.TypeCheck (461ms)
✔ [3348/3381] Built Mathlib.Tactic.Simproc.VecPerm (1.6s)
✔ [3349/3385] Built Mathlib.Data.Finsupp.Weight (4.5s)
✔ [3350/3385] Built Mathlib.Tactic.Simproc.FinsetInterval (3.2s)
✔ [3351/3385] Built ProofWidgets.Component.PenroseDiagram (936ms)
✔ [3352/3386] Built ProofWidgets.Presentation.Expr (861ms)
✔ [3353/3388] Built Mathlib.Tactic.Widget.GCongr (647ms)
✔ [3355/3405] Built ProofWidgets.Component.Panel.Basic (779ms)
✔ [3356/3405] Built Mathlib.Tactic.Widget.CommDiag (1.3s)
✔ [3357/3405] Built ProofWidgets.Component.HtmlDisplay (669ms)
✔ [3358/3405] Built Mathlib.Tactic.WithoutCDot (704ms)
✔ [3359/3405] Built Iut.Stage1.PilotComparison (1.8s)
✔ [3360/3405] Built Iut.Foundations.AlgorithmicOutput (2.1s)
✔ [3361/3405] Built Iut.Foundations.AlgorithmicBridge (3.5s)
✔ [3362/3405] Built Mathlib.RingTheory.MvPowerSeries.Basic (7.9s)
✔ [3363/3405] Built Mathlib.Tactic.Ring.NamePowerVars (1.3s)
✔ [3364/3405] Built Mathlib.Tactic.Widget.StringDiagram (5.0s)
✔ [3365/3405] Built Mathlib.Algebra.Category.Ring.Limits (12s)
✔ [3366/3405] Built Mathlib.Algebra.Category.Ring.Constructions (6.4s)
✔ [3367/3405] Built Mathlib.RingTheory.RingHomProperties (2.2s)
✔ [3368/3405] Built Mathlib.RingTheory.LocalProperties.Basic (3.1s)
✔ [3369/3405] Built Mathlib.RingTheory.LocalProperties.IntegrallyClosed (2.3s)
✔ [3370/3405] Built Mathlib.RingTheory.DedekindDomain.Dvr (1.0s)
✔ [3371/3405] Built Mathlib.RingTheory.Ideal.Norm.AbsNorm (4.7s)
✔ [3372/3405] Built Mathlib.NumberTheory.RamificationInertia.Ramification (4.7s)
✔ [3373/3405] Built Mathlib.NumberTheory.RamificationInertia.Inertia (2.6s)
✔ [3374/3405] Built Mathlib.RingTheory.DedekindDomain.AdicValuation (11s)
✔ [3375/3405] Built Mathlib.FieldTheory.RatFunc.AsPolynomial (4.7s)
✔ [3376/3405] Built Mathlib.NumberTheory.RamificationInertia.Basic (9.3s)
✔ [3377/3405] Built Mathlib.RingTheory.Valuation.Discrete.Basic (5.8s)
✔ [3378/3405] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (4.6s)
✔ [3379/3405] Built Mathlib.RingTheory.Valuation.Discrete.RankOne (3.6s)
✔ [3380/3405] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (3.0s)
✔ [3381/3405] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (2.6s)
✔ [3382/3405] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (4.1s)
✔ [3383/3405] Built Mathlib.RingTheory.DedekindDomain.Factorization (12s)
✔ [3384/3405] Built Mathlib.NumberTheory.Cyclotomic.Basic (9.1s)
✔ [3385/3405] Built Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (3.9s)
✔ [3386/3405] Built Mathlib.NumberTheory.LegendreSymbol.AddCharacter (2.6s)
✔ [3387/3405] Built Mathlib.NumberTheory.NumberField.Completion.FinitePlace (10s)
✔ [3388/3405] Built Mathlib.NumberTheory.GaussSum (3.0s)
✔ [3389/3405] Built Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (1.0s)
✔ [3390/3405] Built Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (1.9s)
✔ [3391/3405] Built Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (2.6s)
✔ [3392/3405] Built Mathlib.Tactic.NormNum.LegendreSymbol (3.4s)
✔ [3393/3405] Built Mathlib.Tactic (1.6s)
✔ [3394/3405] Built Iut.Stage1.CorollarySchema (4.6s)
✔ [3395/3405] Built Iut.Stage1.SourceObligations (2.6s)
✔ [3396/3405] Built Iut.Stage1.IUTSourceScaffold (2.2s)
✔ [3397/3405] Built Iut.Stage1.IUTStage1Data (2.6s)
✔ [3398/3405] Built Iut.Foundations.InitialThetaData (18s)
✔ [3399/3405] Built Iut.Stage1.IUTStage1SourceCore (5.7s)
✔ [3400/3405] Built Iut.Stage1.IUTStage1Remark312Absorption (2.4s)
✔ [3401/3405] Built Iut.Stage1.IUTStage1Source (48s)
✔ [3402/3405] Built Iut.Stage1.IUTStage1Experiments (9.2s)
✔ [3403/3405] Built Iut.Basic (2.4s)
✔ [3404/3405] Built Iut (2.3s)
Build completed successfully (3405 jobs).
semantic_extract exit 0 duration 1h 6m · created 
./.apodeixis/tools/lean-semantic-extract.sh

Keyboard shortcuts