mul_left_cancel

Stream: new members

[toc]

So if I have

m n a : ℤ,
ha : a ≠ 0,
k : ℤ,
h : a * (m * k) = a * n

how on earth do I get m * k = n... I suspect it involves mul_left_cancel or similar but I can't find any straughtforward examples of that in mathlib.

[Bryan Gin-ge Chen]

tactic#library_search is good at finding things like this:

import tactic

example (m n a : ℤ) (ha : a ≠ 0) (k : ℤ) (h : a * (m * k) = a * n) :
m * k = n := by library_search
-- Try this: exact (mul_right_inj' ha).mp h

example (m n a : ℤ) (ha : a ≠ 0) (k : ℤ) (h : a * (m * k) = a * n) :
m * k = n := (mul_right_inj' ha).mp h -- it works!

If you're using VS Code, an interactive suggestion should pop up too.

[toc]

Well that is just 10 kinds of fantastic. I've been using the live editor. Thanks!