Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-09 15:40 20efef78

View on Github →

chore(algebra/field_power, data/set/intervals/basic): simpler proofs in the first file, fewer parentheses in the second one (#7831) This is mostly a cosmetic PR: I removed two calls to linarith, where a term-mode proof was very simple. I also removed some unnecessary parentheses in a different file.

Estimated changes