Zulip Chat Archive

Stream: maths

Topic: reindex_apply


Sebastien Gouezel (Aug 26 2021 at 17:06):

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 (Aug 26 2021 at 17:08):

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

Eric Wieser (Aug 26 2021 at 17:09):

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

Sebastien Gouezel (Aug 26 2021 at 17:10):

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 (Aug 26 2021 at 17:11):

The second one phrased in terms of minor already exists

Eric Wieser (Aug 26 2021 at 17:11):

And is used to define reindex_alg_equiv in the first place

Eric Wieser (Aug 26 2021 at 17:13):

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

Sebastien Gouezel (Aug 26 2021 at 17:16):

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 (Aug 26 2021 at 17:20):

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

Eric Wieser (Aug 26 2021 at 17:31):

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

Eric Wieser (Aug 26 2021 at 17:31):

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

Eric Wieser (Aug 26 2021 at 17:49):

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


Last updated: Dec 20 2023 at 11:08 UTC