mathlib3
a149cb73 - chore(analysis/bounded_variation): replace uses of `linarith` (#17998)

Commit

3 years ago

chore(analysis/bounded_variation): replace uses of `linarith` (#17998) Co-authored-by: Rémi Bottinelli <bottine@users.noreply.github.com>

References

Author

bottine

Parents