Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-09 09:24 d12a7319

View on Github →

chore(data/mv_polynomial): mark mv_polynomial.ext as @[ext] (#5289)

Estimated changes

modified theorem mv_polynomial.ext