Zulip Chat Archive

Stream: new members

Topic: funny lemma


view this post on Zulip Damiano Testa (Apr 14 2021 at 18:36):

Dear All,

while trying to prove something else, I found myself proving the lemma below: would it be of any use to make a PR with it? It feels funny to establish such an iff, and I wonder if anyone else has seen it elsewhere.

Thanks!

lemma abs_add_eq_iff_abs_mul_eq {a b : } : abs (a + b) = abs a + abs b  abs (a * b) = a * b :=
sorry

PS: I have a proof, but I am not writing it, in case you want to play with it yourself!

view this post on Zulip Kevin Buzzard (Apr 14 2021 at 18:38):

These things don't "feel related" to me. I think I'd be tempted to prove abs (a + b) = abs a + abs b ↔ (both non-negative or both non-positive) and product non-negative iff both factors non-negative or non-positive.

view this post on Zulip Damiano Testa (Apr 14 2021 at 19:00):

Yes, the lemma characterizing abs (a + b) = abs a + abs b is already in mathlib. This specific one came up since the LHS was an assumption and the RHS was the goal in a step of a proof in the lean-liquid file.


Last updated: May 11 2021 at 12:15 UTC