mathlib3
58debc0e - chore(data/fintype/basic): golf, generalize to `Sort*` (#17227)

Commit

3 years ago

chore(data/fintype/basic): golf, generalize to `Sort*` (#17227)

Author

urkud

urkud

Parents

Loading