Commit 2025-08-04 22:51 228533c3

View on Github →

feat(RepresentationTheory): add the norm map (#27362) Given a representation A of a finite group G, A.norm is the representation morphism A ⟶ A defined by x ↦ ∑ A.ρ g x for g in G. We define this and prove related lemmas.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

added theorem Fin.partialProd_init

Modified Mathlib/RepresentationTheory/Basic.lean

added theorem Representation.apply_eq_of_leftRegular_eq_of_generator

added theorem Representation.apply_sub_id_partialSum_eq

added theorem Representation.ker_leftRegular_norm_eq

added theorem Representation.leftRegular_norm_apply

added theorem Representation.leftRegular_norm_eq_zero_iff

added def Representation.norm

added theorem Representation.norm_comp_self

added theorem Representation.norm_ofDistribMulAction_eq

added theorem Representation.norm_ofMulDistribMulAction_eq

added theorem Representation.norm_self_apply

added theorem Representation.self_comp_norm

added theorem Representation.self_norm_apply

Modified Mathlib/RepresentationTheory/Rep.lean

added theorem Rep.applyAsHom_comm

added def Rep.norm

added def Rep.normNatTrans

added theorem Rep.norm_comm