reindex_apply

Stream: maths

[Sebastien Gouezel]

We have in the library the lemma

@[simp] lemma reindex_apply (eₘ : m ≃ l) (eₙ : n ≃ o) (M : matrix m n α) :
  reindex eₘ eₙ M = M.minor eₘ.symm eₙ.symm :=
rfl

I am not sure I am convinced by the simp attribute (but I am not experienced at all with the linear algebra part of the library). Any feeling on this?

[Eric Wieser]

The idea here was to avoid having to repeat every lemma about minor for reindex

[Eric Wieser]

If the latter simplifies to the former then that isn't necessary

[Sebastien Gouezel]

Same corner of the library:

@[simp] lemma reindex_alg_equiv_apply (e : m ≃ n) (M : matrix m m R) :
  reindex_alg_equiv R e M = reindex e e M :=
rfl

lemma reindex_alg_equiv_mul (e : m ≃ n) (M : matrix m m R) (N : matrix m m R) :
  reindex_alg_equiv R e (M ⬝ N) = reindex_alg_equiv R e M ⬝ reindex_alg_equiv R e N :=
(reindex_alg_equiv R e).map_mul M N

The first simp lemma ensures that the second one can never be used as a simp lemma. Should the second one be phrased in terms of minors to be usable by simp?

[Eric Wieser]

The second one phrased in terms of minor already exists

[Eric Wieser]

And is used to define reindex_alg_equiv in the first place

[Eric Wieser]

docs#matrix.minor_mul_equiv is that lemma, and it's more general

[Sebastien Gouezel]

Thanks for the pointer! Unfortunately, it is not accepted as a simp lemma (invalid simplification lemma 'matrix.minor_mul_equiv'). I'll work my way by hand, then, tweaking my simp set to make it work.

[Eric Wieser]

I think the argument for having docs#matrix.reindex_alg_equiv_mul was to make rewrites easier, not for simp

[Eric Wieser]

I think the argument for having docs#matrix.reindex_alg_equiv_mul was to make rewrites easier, not for simp

[Eric Wieser]

I think you can just add a simp copy of the minor lemma for when e1 = e2 = e3?

[Eric Wieser]

Since right now it's invalid as e2 appears only on the RHS