Commit 2026-04-03 08:03 1e483c88

View on Github →

chore(RepresentationTheory/FiniteIndex): generalize universes (#37271)

Estimated changes

Modified Mathlib/RepresentationTheory/FiniteIndex.lean

modified theorem Rep.coindResAdjunction_counit_app

modified theorem Rep.coindResAdjunction_homEquiv_apply

modified theorem Rep.coindResAdjunction_homEquiv_symm_apply

modified theorem Rep.coindResAdjunction_unit_app

modified theorem Rep.resIndAdjunction_counit_app

modified theorem Rep.resIndAdjunction_homEquiv_apply

modified theorem Rep.resIndAdjunction_homEquiv_symm_apply

modified theorem Rep.resIndAdjunction_unit_app