Matrix.toLin' vs Matrix.mulVecLin

Stream: mathlib4

[Yury G. Kudryashov]

Which one of docs#Matrix.mulVecLin and docs#Matrix.toLin' is supposed to be the normal form for docs#Matrix.mulVec as a linear map?

[Yury G. Kudryashov]

Note that toLin' has an extra DecidableEq assumption that is only needed for the invFun part of the equivalence.

[Yury G. Kudryashov]

@loogle Matrix.toLin'

[loogle]

:search: Matrix.toLin', Matrix.toLin_eq_toLin', and 61 more

[Yury G. Kudryashov]

@loogle Matrix.mulVecLin

[loogle]

:search: Matrix.mulVecLin, Matrix.mulVecLin_transpose, and 20 more

[Eric Wieser]

The unbundled one should be the normal form I think

[Yury G. Kudryashov]

Then I'll make a PR adding the missing simp lemmas and replacing toLin' with mulVecLin.

[Yury G. Kudryashov]

BTW, should we have a def for matrix nullity?

[Yury G. Kudryashov]

We have one for rank, but for nullity we use the finrank of the kernel of mulVecLin (or toLin')

[Yury G. Kudryashov]

(in fact, we have 3 defs for rank with different codomains)

[Eric Wieser]

I think @Peter Nelson was in the process of refactoring matrix ranks to remove finiteness conditions

[Yury G. Kudryashov]

Remove in which sense?

[Yury G. Kudryashov]

docs#Matrix.rank

[Yury G. Kudryashov]

I see, it assumes fintype for no reason. It should be just m.crank.toNat

[Yury G. Kudryashov]

But this refactor is orthogonal to my question

[Eric Wieser]

(it was in response to your parenthetical)

[Yury G. Kudryashov]

After the refactor, we may still have 3 versions with codomains Cardinal, ENat, and Nat, but Nat version probably won't assume Fintype.

[Yury G. Kudryashov]

UPD: wait, we need Fintype to define mulVec, scratch that.

[Yury G. Kudryashov]

Or do you want to redefine Matrix.rank as the rank of the submodule generated by the columns without mulVec?

[Peter Nelson]

You don’t need mulVec for rank. It is the dimension of the row or column span.

[Yury G. Kudryashov]

I see.