[Merged by Bors] - feat: Add API for AlgEquiv.
#8639
Conversation
erdOne
commented
Nov 27, 2023
erdOne
commented
leanprover-community-mathlib4-bot
added
the
merge-conflict
…lib4 into erd1/algequiv_lemmas
leanprover-community-mathlib4-bot
removed
the
merge-conflict
Mathlib/Algebra/Algebra/Equiv.lean
Outdated
| lemma one_toLinearMap : | ||
| (1 : A₁ ≃ₐ[R] A₁).toLinearMap = 1 := rfl | ||
|
|
||
| /-- The units group of `S →ₐ[R] S` is `S ≃ₐ[R] S` -/ |
There was a problem hiding this comment.
Can you add a cross-reference to the LinearEquiv version we already have?
There was a problem hiding this comment.
Do you mean LinearMap.GeneralLinearGroup.generalLinearEquiv?
There was a problem hiding this comment.
Yes, exactly! In fact, it might be nice to show that (algHomUnitsEquiv.symm f).map (toLinearMapHom R A) = (LinearMap.GeneralLinearGroup.generalLinearEquiv.symm f.toLinearMap) or similar
There was a problem hiding this comment.
I'm not sure where such a lemma should go though, and I don't think this lemma is useful enough to warrant a new file of its own.
There was a problem hiding this comment.
Ah, I hadn't realized there was an import issue. That sounds fair.
erdOne
added
awaiting-author
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
erdOne
added
awaiting-review
and removed
awaiting-author
| (σ ^ n).toLinearMap = σ.toLinearMap ^ n := | ||
| (AlgEquiv.toLinearMapHom R A₁).map_pow σ n | ||
|
|
||
| lemma one_toLinearMap : |
There was a problem hiding this comment.
| lemma one_toLinearMap : | |
| @[simp] lemma one_toLinearMap : |
| lemma pow_toLinearMap (σ : A₁ ≃ₐ[R] A₁) (n : ℕ) : | ||
| (σ ^ n).toLinearMap = σ.toLinearMap ^ n := | ||
| (AlgEquiv.toLinearMapHom R A₁).map_pow σ n |
There was a problem hiding this comment.
Can you add the zpow version too?
There was a problem hiding this comment.
There is no zpow on linear maps.
|
bors d+ Thanks! |
|
✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
AlgEquiv.AlgEquiv.
