rzeta0
rzeta0
I finally managed to get a minimal code example working by: 1. loading the libraries in the html `` 2. establishing the html elements 3. only only then after but...
I'm interested in this too. I have a related problem: ``` example {x : ℝ} (hx: x^2 = 0) : x = 0 := by cancel x at hx ```...
This is interesting, I'd like to know too. You might get an answer here: https://leanprover.zulipchat.com (my best guess is that the hypothesis are contradictory and that is why we can...