Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-24 21:45 4fd263ba

View on Github →

feat(representation_theory/character): characters of representations (#14453)

Estimated changes

Modified src/algebra/category/FinVect.lean

added theorem FinVect.iso.conj_eq_conj

added def FinVect.iso_to_linear_equiv

added def linear_equiv.to_FinVect_iso

Modified src/representation_theory/basic.lean

deleted theorem representation.char_conj

deleted theorem representation.char_mul_comm

deleted theorem representation.char_one

modified theorem representation.dual_apply

added theorem representation.dual_tensor_hom_comm

Created src/representation_theory/character.lean

added theorem fdRep.char_conj

added theorem fdRep.char_dual

added theorem fdRep.char_iso

added theorem fdRep.char_lin_hom

added theorem fdRep.char_mul_comm

added theorem fdRep.char_one

added theorem fdRep.char_tensor

added def fdRep.character

Modified src/representation_theory/fdRep.lean

added theorem fdRep.dual_tensor_iso_lin_hom_hom_hom

added theorem fdRep.iso.conj_ρ

added def fdRep.iso_to_linear_equiv

added def fdRep.ρ