Zulip Chat Archive

Stream: maths

Topic: factoring out a constant from a linear map


view this post on Zulip Joseph Corneli (Apr 10 2019 at 18:47):

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

view this post on Zulip Kevin Buzzard (Apr 10 2019 at 18:48):

that's repeat {mul_add}

view this post on Zulip Joseph Corneli (Apr 10 2019 at 18:49):

thanks

view this post on Zulip 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 ;-)

view this post on Zulip 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
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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 10 2019 at 19:21):

rewrite, don't apply

view this post on Zulip Kevin Buzzard (Apr 10 2019 at 19:22):

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

view this post on Zulip Joseph Corneli (Apr 10 2019 at 19:22):

aha, that's better

view this post on Zulip Kevin Buzzard (Apr 10 2019 at 19:22):

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

view this post on Zulip 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