Diff — Representation theory of finite groups

Revision #2821 → #3283 · back to history

modifiedDegree of a representationa3b8e3422b69

Field	From #2821	To #3283
mathlib.module	Mathlib.LinearAlgebra.Dimension.Free	Mathlib.LinearAlgebra.Dimension.Finrank

addedGroup algebra97ab18d13824

addedKernel of a representation-map074e942e9c54

addedTrace of AB equals trace of BA8bcc00b08eeb

addedCharacter at identity equals dimensiona46d56a8b5b0

addedSemidirect productbf68246d6dd7

addedDihedral groupf232fd905c62

addedComplexification of a real vector space80cd91f403f4

addedYoung tableauc99a969b51d7