Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-01 18:15 6e6e6da6

View on Github →

feat(data/nat/basic): two identities for choose (#1936)

  • feat(data/nat/basic): two identities for choose
  • fix build

Estimated changes