Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-13 01:21 cec81510

View on Github →

refactor(representation_theory/Rep): define ihom concretely (#19170)

Estimated changes

Modified src/representation_theory/Rep.lean

modified theorem Rep.Action_ρ_eq_ρ

added theorem Rep.hom_comm_apply

added theorem Rep.hom_equiv_def

deleted theorem Rep.ihom_coev_app_def

modified theorem Rep.ihom_coev_app_hom

modified theorem Rep.ihom_ev_app_hom

deleted theorem Rep.ihom_map_hom

deleted theorem Rep.ihom_obj_ρ

modified theorem Rep.ihom_obj_ρ_def

added def Rep.monoidal_closed.linear_hom_equiv

added def Rep.monoidal_closed.linear_hom_equiv_comm

modified theorem Rep.monoidal_closed.linear_hom_equiv_comm_hom

modified theorem Rep.monoidal_closed.linear_hom_equiv_comm_symm_hom

modified theorem Rep.monoidal_closed.linear_hom_equiv_hom

modified theorem Rep.monoidal_closed.linear_hom_equiv_symm_hom

deleted theorem Rep.monoidal_closed_curry_hom

deleted theorem Rep.monoidal_closed_uncurry_hom

added theorem Rep.ρ_inv_self_apply

added theorem Rep.ρ_self_inv_apply

Modified src/representation_theory/group_cohomology/resolution.lean