Commit 2026-03-07 22:58 e4fa93f7

View on Github →

feat: definition of a character of a representation (#35100) This PR begins to transfer definitions and theorems about characters from FDRep to Representation. Once #34888 is merged, the theorems involving isomorphisms of representations will be appropriately restated.

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

added theorem Module.finrank_eq_zero_of_subsingleton

Modified Mathlib/RepresentationTheory/Character.lean

added theorem Representation.card_inv_mul_sum_char_eq_finrank

added theorem Representation.card_inv_mul_sum_char_mul_char_eq_finrank

added theorem Representation.char_conj

added theorem Representation.char_dual

added theorem Representation.char_iso

added theorem Representation.char_linHom

added theorem Representation.char_mul_comm

added theorem Representation.char_one

added theorem Representation.char_orthonormal

added theorem Representation.char_tensor

added def Representation.character

Modified Mathlib/RepresentationTheory/Intertwining.lean

added def LinearMap.intertwiningMap_of_isIntertwiningMap

added theorem LinearMap.toIntertwiningMap

modified theorem Representation.IntertwiningMap.coe_neg

added theorem Representation.IntertwiningMap.coe_ofBijective

modified theorem Representation.IntertwiningMap.coe_zsmul

added def Representation.IntertwiningMap.ofBijective

deleted theorem Representation.IntertwiningMap.sub_toLinearMap

modified theorem Representation.IntertwiningMap.toLinearMap_apply

added def Representation.IntertwiningMap.toLinearMapl

Modified Mathlib/RepresentationTheory/Invariants.lean

added def Representation.invariantsEquivIntertwiningMap

added theorem Representation.mem_linHom_invariants_iff_isIntertwining

Modified Mathlib/RepresentationTheory/Irreducible.lean

added theorem Representation.IsIrreducible.finrank_intertwiningMap_self