# Zulip Chat Archive

## Stream: maths

### Topic: Linear algebra

#### Sebastien Gouezel (Nov 04 2019 at 22:09):

I need some bits of linear algebra, and I am really struggling. I had forgotten how hard it is to use a part of the library you are not familiar with! Anyway, I am sure everything is already there to get the following statement, but whenever I start with something I begin to unfold and unfold and I am sure I shouldn't (and I guess I am not even writing it in the correct way).

open_locale classical lemma linear_map.pi_apply_eq {ι : Type u} [fintype ι] {𝕜 : Type u} [discrete_field 𝕜] {E : Type v} [add_comm_group E] [vector_space 𝕜 E] (f : (ι → 𝕜) →ₗ[𝕜] E) (x : ι → 𝕜) : f x = finset.sum finset.univ (λi:ι, x i • (f (λj, if j = i then 1 else 0))) := sorry

Between `constr_self (pi.is_basis_fun 𝕜 ι) f`

or `linear_map.std_basis`

, I don't know where to start!

#### Mario Carneiro (Nov 04 2019 at 22:32):

imports?

#### Reid Barton (Nov 04 2019 at 22:34):

No, start with a copyright header

#### Mario Carneiro (Nov 04 2019 at 22:35):

`import apache`

#### Reid Barton (Nov 04 2019 at 22:38):

More seriously, I think you should first use linearity of `f`

to reduce to the same statement without `f`

#### Reid Barton (Nov 04 2019 at 22:45):

Then I don't know whether it is an existing lemma. It does seem to be `std_basis`

-related somehow. Anyways, it doesn't look very difficult to prove using `sum_mul_boole`

for example

#### Sebastien Gouezel (Nov 05 2019 at 10:46):

I ended up doing the following, avoiding completely the linear algebra basis framework, which is a little bit sad. I would be very happy to see the proper way to write it, possibly replacing `λj, if i = j then 1 else 0`

by something more idiomatic. Imports and header included :) Thanks for the reference to `sum_mul_boole`

.

/- Nice Zulip header -/ import linear_algebra.finite_dimensional universes u v w open_locale classical lemma pi_eq_sum_univ {ι : Type u} [fintype ι] {𝕜 : Type v} [ring 𝕜] (x : ι → 𝕜) : x = finset.sum finset.univ (λi:ι, x i • (λj, if i = j then 1 else 0)) := begin ext k, rw pi.finset_sum_apply, have : finset.sum finset.univ (λ (x_1 : ι), x x_1 * ite (k = x_1) 1 0) = x k, { have := finset.sum_mul_boole finset.univ x k, rwa if_pos (finset.mem_univ _) at this }, rw ← this, apply finset.sum_congr rfl (λl hl, _), simp only [smul_eq_mul, mul_ite, pi.smul_apply], conv_lhs { rw eq_comm }, end set_option class.instance_max_depth 36 lemma linear_map.pi_apply_eq_sum_univ {ι : Type u} [fintype ι] {𝕜 : Type v} [discrete_field 𝕜] {E : Type w} [add_comm_group E] [vector_space 𝕜 E] (f : (ι → 𝕜) →ₗ[𝕜] E) (x : ι → 𝕜) : f x = finset.sum finset.univ (λi:ι, x i • (f (λj, if i = j then 1 else 0))) := begin conv_lhs { rw [pi_eq_sum_univ x, f.map_sum] }, apply finset.sum_congr rfl (λl hl, _), rw f.map_smul end

#### Miguel Raz Guzmán Macedo (Nov 14 2019 at 03:58):

@Kevin Buzzard I believe Terence Tao is unwittingly giving Lean a shoutout...

https://twitter.com/InertialObservr/status/1194826080005148672

Apparently an equivalent result has been used/discovered before, but as Terry Tao states it was never published. ... oops https://twitter.com/InertialObservr/status/1194826080005148672/photo/1

- 〈 Berger | Dillon 〉 (@InertialObservr)#### Johan Commelin (Nov 14 2019 at 05:05):

More specifically, I guess you are referring to the following comment by Tao on his blog: https://terrytao.wordpress.com/2019/08/13/eigenvectors-from-eigenvalues/#comment-528704 where he writes:

(It’s at times like this that I wish we had a good semantic search engine for mathematics – I am not sure how I would have discovered this preprint other than by publishing our own preprint and waiting for someone to notice the connection.)

#### Miguel Raz Guzmán Macedo (Nov 14 2019 at 20:59):

Yup that same one @Johan Commelin

Last updated: May 14 2021 at 19:21 UTC