Mathlib Changelog
v3
Changelog
About
Github
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.ρ