New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebra/algebra/{basic,tower}): add alg_equiv.comap and alg_equiv.restrict_scalars #6548
Conversation
src/ring_theory/algebra_tower.lean
Outdated
inv_fun := λ fg, @is_scalar_tower.restrict_base A _ _ _ _ _ _ _ _ _ | ||
fg.1.to_ring_hom.to_algebra _ _ _ _ fg.2, | ||
inv_fun := λ fg, | ||
let alg := fg.1.to_ring_hom.to_algebra in by exactI fg.2.restrict_base A, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This one was fine with the underscores, but is much less fragile to argument reordering this way.
7478e27
to
16d2c2a
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me, thanks!
bors r+
…v.restrict_scalars (#6548) This also renames `is_scalar_tower.restrict_base` to `alg_hom.restrict_scalars`, to enable dot notation and match `linear_map.restrict_scalars`.
Pull request successfully merged into master. Build succeeded: |
…v.restrict_scalars (#6548) This also renames `is_scalar_tower.restrict_base` to `alg_hom.restrict_scalars`, to enable dot notation and match `linear_map.restrict_scalars`.
This also renames
is_scalar_tower.restrict_base
toalg_hom.restrict_scalars
, to enable dot notation and matchlinear_map.restrict_scalars
.