Map

How this project builds on itself. An arrow goes from a file to a file that uses something in it, so the foundations are on the left. These links come from names in the source code, not from kernel dependency facts; the separate Trust page says exactly what Lean checked. every declaration's own map, on its file page, shows the same thing one result at a time.

Files as a table

The same map data in a searchable keyboard- and screen-reader-friendly form.

Files and cross-file dependency counts
FileDeclarationsBuilds onUsed by
APNOutputs/AICollaborator/AdditiveCombinatorics/57.lean10400
APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean4206
APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean3710
APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean5710
APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_4.lean7210
APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean13710
APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean5110
APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean4710
APNOutputs/AICollaborator/Graphs/GraphConjecture2.lean3400
APNOutputs/AICollaborator/Graphs/bipartite_graph_reconstruction_conjecture_2.lean6800
APNOutputs/AICollaborator/Optimization/LastIterateConvergence.lean3500
APNOutputs/AICollaborator/QuantumOptics/35.lean19200
APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean7000
APNOutputs/ErdosProblems/erdos_12.parts.i.lean8001
APNOutputs/ErdosProblems/erdos_12.parts.ii.lean3110
APNOutputs/ErdosProblems/erdos_125.variants.positive_lower_density.lean1900
APNOutputs/ErdosProblems/erdos_138.variants.difference.lean2900
APNOutputs/ErdosProblems/erdos_152.lean6400
APNOutputs/ErdosProblems/erdos_26.variants.tenenbaum.lean7200
APNOutputs/ErdosProblems/erdos_741.parts.i.lean12100
APNOutputs/ErdosProblems/erdos_741.parts.ii.lean3900
APNOutputs/ErdosProblems/erdos_846.lean5400
APNOutputs/OEIS/A224515_conjecture_existence.lean2700
APNOutputs/OEIS/A309132_conjecture_carmichael.lean3200
APNOutputs/OEIS/A382590_conjecture_kth_prime_factor_is_eventually_periodic.lean2100
APNOutputs/OEIS/a091669_conjecture_primitive_root.lean1600
APNOutputs/OEIS/a325046_odd_terms_at_k_times_k_plus_1.lean1400
APNOutputs/OEIS/oeis_103311_conjecture_0.lean2100
APNOutputs/OEIS/oeis_108_conjecture_2.lean3100
APNOutputs/OEIS/oeis_113254_conjecture_0.lean1100
APNOutputs/OEIS/oeis_175386_conjecture_0.lean2700
APNOutputs/OEIS/oeis_194806_conjecture_0.lean2700
APNOutputs/OEIS/oeis_227582_conjecture_0.lean3900
APNOutputs/OEIS/oeis_228143_conjecture_1.lean7700
APNOutputs/OEIS/oeis_243106_conjecture_0.lean700
APNOutputs/OEIS/oeis_248802_conjecture_0.lean1600
APNOutputs/OEIS/oeis_248802_conjecture_4.lean7800
APNOutputs/OEIS/oeis_256012_conjecture_0.lean700
APNOutputs/OEIS/oeis_267581_conjecture_0.lean1300
APNOutputs/OEIS/oeis_271591_conjecture_0.lean3100
APNOutputs/OEIS/oeis_278070_conjecture_0.lean200
APNOutputs/OEIS/oeis_282779_conjecture_0.lean600
APNOutputs/OEIS/oeis_289411_conjecture_0.lean1400
APNOutputs/OEIS/oeis_2897_conjecture_0.lean4000
APNOutputs/OEIS/oeis_306424_conjecture_0.lean1800
APNOutputs/OEIS/oeis_307865_conjecture_0.lean1200
APNOutputs/OEIS/oeis_323557_conjecture_0.lean1500
APNOutputs/OEIS/oeis_340737_conjecture_0.lean5400
APNOutputs/OEIS/oeis_341254_conjecture_0.lean1700
APNOutputs/OEIS/oeis_363347_conjecture_2.lean6900
APNOutputs/OEIS/oeis_372761_conjecture_2.lean4700
APNOutputs/OEIS/oeis_51293_conjecture_0.lean5700
APNOutputs/OEIS/oeis_62567_conjecture_0.lean3500
APNOutputs/OEIS/oeis_A028859_conjecture_1.lean5600
APNOutputs/OEIS/oeis_A258667_conjecture_0.lean5400
APNOutputs/OEIS/oeis_a211417_conjecture_specific.lean3100
APNOutputs/OEIS/oeis_a237271_conjecture_2.lean400
APNOutputs/OEIS/oeis_a300997_finite_difference_is_one_or_two.lean8100
APNOutputs/OEIS/oeis_a363102_conjecture_1.lean2300
APNOutputs/OEIS/oeis_a368692_conjecture_integrality.lean1000
APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_of_directed_colimit.lean2003
APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_transitive.lean1610
APNOutputs/StacksProject/AlgebrasOverFields_geometrically_irreducible_tfae.lean7610
APNOutputs/StacksProject/AlgebrasOverFields_minimalPrimes_bijection_of_geometrically_IrreducibleAlgebra.lean2910
APNOutputs/StacksProject/AlgebrasOverFields_unique_minimal_prime_of_tensor_product_of_separably_closed.lean5300
APNOutputs/StacksProject/GeometricallyReduced_isGeometricallyReduced_iff_of_separable_algebraic.lean5903
APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separable.lean3210
APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separablyGenerated.lean6710
APNOutputs/StacksProject/NormalRings_NormalDomain_powerSeries.lean2801
APNOutputs/StacksProject/NormalRings_normalRing_characterization.lean4710
APNOutputs/StacksProject/Separability_exists_isPurelyInseparable_isSeparablyGenerated_of_essFiniteType.lean9810