Zulip Chat Archive

Stream: new members

Topic: mul_left_cancel


view this post on Zulip toc (Sep 03 2020 at 15:22):

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.

view this post on Zulip Bryan Gin-ge Chen (Sep 03 2020 at 15:24):

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.

view this post on Zulip toc (Sep 03 2020 at 15:26):

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


Last updated: May 08 2021 at 03:17 UTC