mathlib3
[Merged by Bors] - refactor(representation_theory/Rep): define `ihom` concretely
#19170
Closed
Overview
Commits
3
Changes
View On GitHub

[Merged by Bors] - refactor(representation_theory/Rep): define `ihom` concretely #19170

101damnations wants to merge 3 commits into master from Rep_ihom_refactor
101damnations
make ihom more concrete
50294682
101damnations 101damnations added awaiting-review
101damnations 101damnations added awaiting-CI
github-actions github-actions removed awaiting-CI
fix indentation
3f3a3b5d
add lemmas that are useful for porting
15f86f47
joelriou
kim-em
github-actions github-actions added ready-to-merge
github-actions github-actions removed awaiting-review
bors
bors bors changed the title refactor(representation_theory/Rep): define `ihom` concretely [Merged by Bors] - refactor(representation_theory/Rep): define `ihom` concretely 3 years ago
bors bors closed this 3 years ago
bors bors deleted the Rep_ihom_refactor branch 3 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum