# Zulip Chat Archive

## Stream: general

### Topic: Refactoring `linear_map <-> matrix`

#### Anne Baanen (Sep 29 2020 at 11:15):

Here's a refactor I would like to propose, to standardise and simplify going from matrices to linear maps and vice versa.

`linear_map.to_matrix`

will be the main definition, an equivalence between`M₁ →ₗ[R] M₂`

and`matrix m n R`

, given bases for`M₁`

and`M₂`

.`matrix.to_lin`

is`linear_map.to_matrix.symm`

`linear_map.to_matrix'`

and`matrix.to_lin'`

are the equivalences between`((n → R) →ₗ[R] (m → R))`

and`matrix m n R`

in the respective directions- we keep
`matrix.mul_vec`

because its definition comes before`linear_map`

- other auxiliary definitions (e.g. the current
`linear_map.to_matrixₗ`

) will be`simp`

ed to the above.

(The current situation is that we have `matrix.mul_vec`

, `matrix.eval`

, `matrix.to_lin`

, `linear_map.to_matrixₗ`

, `linear_map.to_matrix`

, `linear_equiv_matrix'`

and `linear_equiv_matrix`

, each with various choices among `→`

, `→ₗ`

and `≃ₗ`

for the arrows. The most powerful, `linear_equiv_matrix`

, is also the most inconvenient to type.)

#### Patrick Massot (Sep 29 2020 at 11:52):

I don't know what is the solution, but I very much agree that what we currently have is a mess that is very hard to navigate.

#### Anne Baanen (Sep 29 2020 at 15:18):

`linear_algebra/matrix.lean`

compiles again: https://github.com/leanprover-community/mathlib/commit/b0375d38069d44dae15e78589bc0ab97137b6437

#### Johan Commelin (Sep 29 2020 at 15:19):

Cool!

#### Anne Baanen (Oct 05 2020 at 14:20):

Two more refactorings I would like to propose now #4345 is merged:

- split
`linear_algebra/basic.lean`

and`linear_algebra/basis.lean`

into more manageably sized files - rename
`module_equiv_finsupp`

to`is_basis.repr`

(replacing the previous`is_basis.repr`

) and figure out what to do with`is_basis.equiv_fun`

#### Patrick Massot (Oct 05 2020 at 14:27):

I don't understand the second point. We still need a version that applies in infinite dimensions, right?

#### Patrick Massot (Oct 05 2020 at 14:27):

And of course I agree with the first point and I'm very grateful for your cleaning efforts.

#### Anne Baanen (Oct 05 2020 at 14:28):

Sorry, that should be `module_equiv_finsupp`

instead of `is_basis.equiv_fun`

.

#### Patrick Massot (Oct 05 2020 at 14:31):

Ok. It would be nice to figure out how to make that parallel track thing (finsupp vs function) less painful.

Last updated: May 13 2021 at 18:26 UTC