mathlib3
dfcbe856 - refactor(data/finite): move definition to a new file (#15204)

Commit

3 years ago

refactor(data/finite): move definition to a new file (#15204) The new file imports nothing but `logic.equiv.basic`.

Author

urkud

Parents