Zulip Chat Archive

Stream: general

Topic: conv in sum


view this post on Zulip Morenikeji Neri (Aug 01 2018 at 15:52):

I would like to show

finset.sum finset.univ  (λ (μ : S n), e (ρ.to_fun) * e (μ.to_fun) * finset.prod finset.univ (λ (i : fin n), A (μ.to_fun i) i)) = finset.sum finset.univ
      (λ (μ : S n), e (ρ.to_fun) * (e (μ.to_fun) * finset.prod finset.univ (λ (i : fin n), A (μ.to_fun i) i)))

where multiplication is in a comm_ring hence is associative, however I cannot use conv as it cannot synthesis μ.to_fun as it is a function. Any tips?

view this post on Zulip Morenikeji Neri (Aug 01 2018 at 16:29):

all sorted

view this post on Zulip Simon Hudon (Aug 01 2018 at 16:39):

I recommend you make a minimal working example so that people can have a look inside of a Lean session.

I think congr' 1, ext, rw mul_assoc could help.


Last updated: May 17 2021 at 21:12 UTC