Theorem FDRep.endRingEquiv_comp_ρ

Modification history

2025-02-28 11:19
Mathlib/RepresentationTheory/FDRep.lean
chore(RepresentationTheory): generalize most of FDRep to commutative rings (#22235)
Modified FDRep.endRingEquiv_comp_ρView on Github →
2025-01-26 18:07
Mathlib/RepresentationTheory/FDRep.lean
feat(Algebra): `Mul/RingEquiv`s between `center` and `Module.End` (#20721)
Added FDRep.endRingEquiv_comp_ρView on Github →