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
MIL/C01_Introduction/S02_Overview.lean400
MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean1811
MIL/C02_Basics/solutions/Solutions_S03_Using_Theorems_and_Lemmas.lean200
MIL/C02_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean400
MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean1300
MIL/C03_Logic/S02_The_Existential_Quantifier.lean800
MIL/C03_Logic/S03_Negation.lean400
MIL/C03_Logic/S04_Conjunction_and_Iff.lean200
MIL/C03_Logic/S06_Sequences_and_Convergence.lean911
MIL/C04_Sets_and_Functions/S01_Sets.lean300
MIL/C04_Sets_and_Functions/S02_Functions.lean300
MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean701
MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean400
MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean1701
MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean1301
MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean1600
MIL/C06_Discrete_Mathematics/S01_Finsets_and_Fintypes.lean200
MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean300
MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean2901
MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean1010
MIL/C07_Structures/S01_Structures.lean3011
MIL/C07_Structures/S02_Algebraic_Structures.lean1301
MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean4011
MIL/C07_Structures/solutions/Solutions_S01_Structures.lean611
MIL/C07_Structures/solutions/Solutions_S02_Algebraic_Structures.lean810
MIL/C08_Hierarchies/S01_Basics.lean4401
MIL/C08_Hierarchies/S02_Morphisms.lean1300
MIL/C08_Hierarchies/S03_Subobjects.lean501
MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean1110
MIL/C08_Hierarchies/solutions/Solutions_S03_Subobjects.lean310
MIL/C09_Groups_and_Rings/S01_Groups.lean1600
MIL/C09_Groups_and_Rings/S02_Rings.lean810
MIL/C11_Topology/S01_Filters.lean300
MIL/C03_Logic/S05_Disjunction.lean500
MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean500
MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean710
MIL/C07_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean611
MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean310
MIL/C09_Groups_and_Rings/solutions/Solutions_S01_Groups.lean800
MIL/C11_Topology/S02_Metric_Spaces.lean100
MIL/C11_Topology/solutions/Solutions_S02_Metric_Spaces.lean100
MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean710
MIL/C09_Groups_and_Rings/solutions/Solutions_S02_Rings.lean601
MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean200
MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean1211
MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean200
MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean100
MIL/C02_Basics/solutions/Solutions_S04_More_on_Order_and_Divisibility.lean100
MIL/C03_Logic/solutions/Solutions_S06_Sequences_and_Convergence.lean511
MIL/C03_Logic/solutions/Solutions_S04_Conjunction_and_Iff.lean100
MIL/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean100
MIL/C10_Linear_Algebra/S02_Subspaces.lean100
MIL/C10_Linear_Algebra/solutions/Solutions_S02_Subspaces.lean100
MIL/C08_Hierarchies/solutions/Solutions_S02_Morphisms.lean100
MIL/C11_Topology/S03_Topological_Spaces.lean100
MIL/C11_Topology/solutions/Solutions_S03_Topological_Spaces.lean100