mathlib
20efef78 - chore(algebra/field_power, data/set/intervals/basic): simpler proofs in the first file, fewer parentheses in the second one (#7831)

Commit
4 years ago
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.
Author
Parents
Loading