> 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...

So, you think it's important for other people to learn Lean's model of type theory before using it to do entirely unrelated proofs, but you see no reason you should know anything about how basic arithmetic works?