mathlib
473ee9e0 - chore(zmod/basic): remove unneeded import (#18856)

Commit

2 years ago

chore(zmod/basic): remove unneeded import (#18856) This file was importing a weird dependency; I am now minimising this.

Author

ericrbg

Parents