mathlib3

0bd2ea37 - refactor(data/fin/basic): fin refactor to use ne_zero (#18107)

refactor(data/fin/basic): fin refactor to use ne_zero (#18107) Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>