[Merged by Bors] - feat(linear_algebra/basis) remove several [nontrivial R] #7642
Conversation
riccardobrasca
added
the
awaiting-review
src/linear_algebra/basis.lean
Outdated
| def reindex_range [nontrivial R] : basis (range b) R M := | ||
| b.reindex (equiv.of_injective b b.injective) | ||
| def reindex_range : basis (range b) R M := | ||
| begin |
There was a problem hiding this comment.
I am not sure it is OK to use tactic mode in a def.
There was a problem hiding this comment.
Hmm, I'm not sure this is a good idea. It would be nice if we can avoid by_cases in this definition.
There was a problem hiding this comment.
Let me see if there is a better proof.
There was a problem hiding this comment.
I think this is fine. The lemmas below show that you can still reason about the value of this definition. You could also use or.by_cases in term mode, but you will probably end up with the same / a similar term.
There was a problem hiding this comment.
Personally, I would prefer if for definitions:
if h : nontrivial R then
by exactI
...
else
by haveI : subsingleton R := ...; exact
...There was a problem hiding this comment.
I like the if! I have the impression we have to reason by cases, in a way or another: the two proofs are really different. Indeed if R is trivial this is true just because anything is a basis (and the rank is not well defined!).
| b.reindex_range ⟨b i, h⟩ = b i := | ||
| by rw [reindex_range, reindex_apply, equiv.apply_of_injective_symm b b.injective, subtype.coe_mk] | ||
| begin | ||
| by_cases htr : nontrivial R, |
There was a problem hiding this comment.
You might be able to use the nontriviality tactic to automatically do the not-nontrivial case for you.
|
✌️ riccardobrasca can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors r+ |
|
Canceled. |
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
|
bors r+ |
We remove some unnecessary `nontrivial R`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
We remove some unnecessary `nontrivial R`.
We remove some unnecessary
nontrivial R.