## Stream: maths

### Topic: factoring out a constant from a linear map

#### Joseph Corneli (Apr 10 2019 at 18:47):

Is there a notion in mathlib that a(x+y+z+...)=ax+ay+az+...?

#### Kevin Buzzard (Apr 10 2019 at 18:48):

that's repeat {mul_add}

thanks

#### Kevin Buzzard (Apr 10 2019 at 18:55):

It's got some official name too, something like left_distrib or right_distrib, but mul_add is a lot easier to remember ;-)

#### Joseph Corneli (Apr 10 2019 at 19:20):

Hm... not having much success with it.

import data.real.basic
open real

lemma factor_two (a x y : ℝ) : a*(x+y) = a * x + a * y  :=
begin
end

lemma factor_three (a x y z : ℝ) : a*(x+y+z) = a * x + a * y + a * z  :=
begin
end


#### Joseph Corneli (Apr 10 2019 at 19:21):

tactic failed, there are unsolved goals
state:
a x y z : ℝ
⊢ a * (x + y + z) = a * x + a * y + a * z

#### Kevin Buzzard (Apr 10 2019 at 19:21):

rewrite, don't apply

#### Kevin Buzzard (Apr 10 2019 at 19:22):

apply only works when the goal is exactly the target of mul_add

#### Joseph Corneli (Apr 10 2019 at 19:22):

aha, that's better

#### Kevin Buzzard (Apr 10 2019 at 19:22):

sorry, my bad, trying to do too many things at once.

#### Joseph Corneli (Apr 10 2019 at 19:24):

no worries! Still much faster than me monkey-typing here.

Last updated: May 09 2021 at 10:11 UTC