[Merged by Bors] - chore(RingTheory/TensorProduct): golf #7539
Conversation
…`AlgHom.ofLinearMap` The former previously took a hypothesis about `f (algebraMap R A r) = algebraMap R B r`, but now needs only `f 1 = 1`, matching the latter. This doesn't make much difference at the two callers.
This adds `LinearMap.map_mul_iff` to match the existing `AddMonoidHom.map_mul_iff`, and uses it to golf some results.
eric-wieser
added
awaiting-review
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
| letI : Algebra R C := RestrictScalars.algebra R S C | ||
| letI : IsScalarTower R S C := RestrictScalars.isScalarTower R S C |
There was a problem hiding this comment.
Should these be just plain lets?
| letI : Algebra R C := RestrictScalars.algebra R S C | |
| letI : IsScalarTower R S C := RestrictScalars.isScalarTower R S C | |
| let _i1 : Algebra R C := RestrictScalars.algebra R S C | |
| let _i2 : IsScalarTower R S C := RestrictScalars.isScalarTower R S C |
(Even after reading the tactic documentation I don't fully understand when I'll need to the inlining that letI provides.)
There was a problem hiding this comment.
This was a combination of lean 3 muscle memory, and an unwillingness to have to name these.
I suspect that there are still good reasons to use letI for instances as a general rule, but indeed it makes no difference here
There was a problem hiding this comment.
I'm going to leave these as letIs because it matches the mathportisms that are already endemic to mathlib4; but as you saw I created https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/let.20vs.20letI.20for.20local.20instances/near/396246664 to revisit this.
|
✌️ 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 |
This adds `LinearMap.map_mul_iff` to match `AddMonoidHom.map_mul_iff` and uses it (along with `AlgHom.ofLinearMap`) to golf away some induction proof in favor of `ext`. The main motivation is the `map_mul_iff` lemma itself, not the golfing. Also fixes some incorrect docstrings that were mangled during porting, and adds an explicit name to an instance.
|
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
This adds `LinearMap.map_mul_iff` to match `AddMonoidHom.map_mul_iff` and uses it (along with `AlgHom.ofLinearMap`) to golf away some induction proof in favor of `ext`. The main motivation is the `map_mul_iff` lemma itself, not the golfing. Also fixes some incorrect docstrings that were mangled during porting, and adds an explicit name to an instance.
This adds
LinearMap.map_mul_iffto matchAddMonoidHom.map_mul_iffand uses it (along withAlgHom.ofLinearMap) to golf away some induction proof in favor ofext.The main motivation is the
map_mul_ifflemma itself, not the golfing.Also fixes some incorrect docstrings that were mangled during porting, and adds an explicit name to an instance.
AlgEquiv.ofLinearEquivwithAlgHom.ofLinearMap#7537