mathlib
adcd09d1 - chore(tactic/linarith): remove final linting error (#3196)

Commit

5 years ago

chore(tactic/linarith): remove final linting error (#3196) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author

robertylewis

Parents