Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-08 08:25 18246ac4

View on Github →

refactor(category_theory/finite_limits): reorganise import hierarchy (#3320) Previously, all of the "special shapes" that happened to be finite imported category_theory.limits.shapes.finite_limits. Now it's the other way round, which I think ends up being cleaner. This also results in some significant reductions to the dependency graph (e.g. talking about homology of complexes no longer requires compiling data.fintype.basic and all its antecedents). No actual content, just moving content around.

Estimated changes