Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-10 00:03 18b378d8

View on Github →

chore(data/fin): reorder file to group declarations (#6109) The data/fin file has a lot of definitions and lemmas. This reordering groups declarations and places ones that do not rely on fin operations first, like order. No definitions or lemma statements have been changed. A minimal amount of proofs have been rephrased. No reformatting of style has been done. Section titles have been added. This is useful in preparation for redefining fin operations (lean#527). Additionally, it allows for better organization for other refactors like making pred and pred_above total.

Estimated changes