Commit 2025-02-28 11:19 c79faca1

View on Github →

chore(RepresentationTheory): generalize most of FDRep to commutative rings (#22235)

Estimated changes

Modified Mathlib/RepresentationTheory/FDRep.lean

modified theorem FDRep.Iso.conj_ρ

modified theorem FDRep.endRingEquiv_comp_ρ

modified theorem FDRep.endRingEquiv_symm_comp_ρ

modified def FDRep.forget₂HomLinearEquiv

modified theorem FDRep.forget₂_ρ

modified theorem FDRep.hom_action_ρ

modified def FDRep.isoToLinearEquiv

modified def FDRep.ρ