min_max): minimum and maximum over list (#884)

Commit

6 years ago

feat(data/list/min_max): minimum and maximum over list (#884) * feat(data/list/min_max): minimum and maximum over list * Update min_max.lean * replace semicolons

References

#884 - feat(data/list/min_max): minimum and maximum over list

Author

minchaowu

Committer

mergify[bot]

Parents

858d111c

mathlib 901bdbf4 - feat(data/list/min_max): minimum and maximum over list (#884)

mathlib
901bdbf4 - feat(data/list/min_max): minimum and maximum over list (#884)