[Merged by Bors] - chore(Data/Matrix/Invertible): generalize conjugate and transpose lemmas #6618
Conversation
These lemmas are more general than the one about `nonsing_inv`
eric-wieser
added
awaiting-review
eric-wieser
changed the title
| /-- Together `Matrix.invertibleTranspose` and `Matrix.invertibleOfInvertibleTranspose` form an | ||
| equivalence, although both sides of the equiv are subsingleton anyway. -/ | ||
| @[simps] | ||
| def transposeInvertibleEquivInvertible : Invertible Aᵀ ≃ Invertible A where |
There was a problem hiding this comment.
I'm not sure about this equiv. Will it ever be used except for your proof of isUnit_transpose below?
There was a problem hiding this comment.
Probably not, but this result is one that we already had in the other file, and I've somewhat established this pattern across the matrix inversion bits of the library, even though I admit it's not a very nice one.
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
bors merge |
…mas (#6618) The `conjTranspose` lemmas now work for non-commutative rings.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
The
conjTransposelemmas now work for non-commutative rings.