## Stream: general

### Topic: conv in sum

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

all sorted

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