Stream: new members
Donald Sebastian Leung (Feb 25 2020 at 07:06):
So I want to prove the following goal:
(1 : ℝ) / 10 ≠ 1. Is there any automated tactic (in stdlib/mathlib) capable of solving the following goal immediately, or would I have to prove it from first principles?
Kevin Buzzard (Feb 25 2020 at 07:11):
Donald Sebastian Leung (Feb 25 2020 at 08:20):
Kevin Buzzard said:
That did the trick, thanks!
Last updated: May 11 2021 at 00:31 UTC