Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-11 12:19 be79f9f3

View on Github →

chore(data/cardinal): put embedding into cardinal namespace

Estimated changes