Mathlib Changelog
v4
Changelog
About
Github
Theorem
Representation.apply_sub_id_partialSum_eq
Modification history
2025-08-04 22:51
Mathlib/RepresentationTheory/Basic.lean
feat(RepresentationTheory): add the norm map (#27362) …
Added
Representation.apply_sub_id_partialSum_eq
View on Github →