-
Notifications
You must be signed in to change notification settings - Fork 297
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
example for #14308 #14372
example for #14308 #14372
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…morrison/Rep-equiv
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
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 is interesting, thank you, it's so concise. Are there any particular aspects you'd recommend me incorporating into #14308 now - maybe an explicit definition of the diagonal & left regular mul_actions as Actions (+ the Reps they induce) - or would it be better to wait for the PRs #14372 depends on and refactor then?
@101damnations, not a serious suggestion that you adopt this approach, but for you interest this was my attempt at the "fancy" way to do some of what you have in #14308.
This depends on several PRs already in the queue, so please just look at
src/representation_theory/example.lean
.