funny lemma

Stream: new members

[Damiano Testa]

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!

[Kevin Buzzard]

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.

[Damiano Testa]

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.