mathlib
92ac50cb - chore(data/finset): rename le_min_of_mem to min_le_of_mem (#1231)

Commit

6 years ago

chore(data/finset): rename le_min_of_mem to min_le_of_mem (#1231) * chore(data/finset): rename le_min_of_mem to min_le_of_mem * fix build

References

Author

ChrisHughes24

Committer

mergify[bot]

Parents