> No, 1/0 is not 0 in lean.

1/0 is 0 in lean, though it may not be a problem. https://xenaproject.wordpress.com/2020/07/05/division-by-zer...