# Zulip Chat Archive

## Stream: new members

### Topic: funny lemma

#### 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!

#### 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.

#### 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