Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-09 11:36 fea68aac

View on Github →

chore(data/fintype/basic): documenting elaboration bug (#11247) Simplifying an expression and documenting an elaboration bug that it was avoiding.

Estimated changes