factoring out a constant from a linear map

Stream: maths

[Joseph Corneli]

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

[Kevin Buzzard]

that's repeat {mul_add}

[Joseph Corneli]

thanks

[Kevin Buzzard]

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]

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
apply mul_add, -- yay
end

lemma factor_three (a x y z : ℝ) : a*(x+y+z) = a * x + a * y + a * z  :=
begin
repeat {apply mul_add}, -- ?
end

[Joseph Corneli]

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

[Kevin Buzzard]

rewrite, don't apply

[Kevin Buzzard]

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

[Joseph Corneli]

aha, that's better

[Kevin Buzzard]

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

[Joseph Corneli]

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