mathlib
c42aaa3d - chore(data/pi): add missing `pi.{inv,neg}_def` (#9361)

Commit

4 years ago

chore(data/pi): add missing `pi.{inv,neg}_def` (#9361)

Author

eric-wieser

eric-wieser

Parents

Loading