[Merged by Bors] - feat(data/matrix/basic): dependently-typed block diagonal #7068
Conversation
src/data/matrix/basic.lean
Outdated
| { subst h, | ||
| convert (fintype.sum_eq_single k (λ i hi, _)).symm, | ||
| { congr' 1, | ||
| ext x, | ||
| simp, }, | ||
| simp [dif_neg hi, dif_neg hi.symm], }, | ||
| { symmetry, | ||
| apply fintype.sum_eq_zero, | ||
| intro i, | ||
| apply fintype.sum_eq_zero, | ||
| intro x, | ||
| rcases decidable.em (k = i) with rfl | hki, | ||
| { simp [dif_neg h] }, | ||
| rcases decidable.em (i = k') with rfl | hik', | ||
| { simp [dif_neg h] }, | ||
| { simp [dif_neg hki, dif_neg hik'] } } |
There was a problem hiding this comment.
simp [h] could close this for the non-dependent form :(
eric-wieser
added
the
awaiting-review
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
Vierkantor
added
delegated
|
@Vierkantor, thoughts on writing the unprimed version in terms of the primed one? |
I don't have a strong opinion: if it saves duplicate lines and the dependentness doesn't leak through the API, then it should be a good idea. Otherwise I don't expect that the two copies really cause too much duplication: the first thing I would do is to define a |
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
That's a good idea - I'll leave that and my suggestion to merge the non-dependent one for a follow-up. |
|
bors r+ |
github-actions
bot
added
the
ready-to-merge
This allows constructing block diagonal matrices whose blocks are different sizes. A notable example of such a matrix is the one from the Jordan Normal Form. This duplicates all of the API for `block_diagonal` from this file. Most of the proofs copy across cleanly, but the proof for `block_diagonal_mul'` required lots of hand-holding that `simp` could solve by itself for the non-dependent case.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This allows constructing block diagonal matrices whose blocks are different sizes. A notable example of such a matrix is the one from the Jordan Normal Form.
This duplicates all of the API for
block_diagonalfrom this file. Most of the proofs copy across cleanly, but the proof forblock_diagonal_mul'required lots of hand-holding thatsimpcould solve by itself for the non-dependent case.For reviewers: Should I prove all the non-dependent lemmas by rewriting along
block_diagonal'_eq_block_diagonal?Zulip thread