Commit 2023-07-03 11:03 9c8d5b1c

View on Github →

feat: port RepresentationTheory.Character (#5679)

Estimated changes

added theorem FdRep.char_conj
added theorem FdRep.char_dual
added theorem FdRep.char_iso
added theorem FdRep.char_linHom
added theorem FdRep.char_mul_comm
added theorem FdRep.char_one
added theorem FdRep.char_orthonormal
added theorem FdRep.char_tensor'
added theorem FdRep.char_tensor
added def FdRep.character