mul_left_cancel on reals

Stream: Is there code for X?

[Colin Jones ⚛️]

Is there a lemma like mul_left_cancel but for real numbers? When I use this lemma for real numbers, it doesn't seem to work for some reason and keeps giving an error : "failed to synthesize instance IsLeftCancelMul ℝ". Could someone give me a fix or an alternative?

Below is my code:
Why_wont_mul_left_cancel_work.lean

[Scott Morrison]

Please post code as code blocks, with complete imports. See #mwe!

[Damiano Testa]

Does docs#mul_left_cancel₀ help?

[Riccardo Brasca]

Damiano's answer is the correct one, docs#mul_left_cancel doesn't work for real numbers because it is false! 0*0=0*1. In general we add a little ₀ to the name of a lemma for the version that says "if a ≠ 0 then ...".

[Colin Jones ⚛️]

Thanks Riccardo! My code works perfectly now