\import Algebra.Group
\import Algebra.Group.Representation
\import Algebra.Linear.Matrix
\import Algebra.Module.LinearMap
\import Algebra.Module.Trace
\import Algebra.Ring
\import Meta
\import Paths.Meta

\func Character {R : Ring}{G : Group}(E : LinRepres R G)
                {lv : Array E} (bv : E.IsBasis lv)
                (g : G) : R => Trace (LinearMap.toMatrix lv bv (E.toLinearMap g))
    \where {
      \protected \func chi (g : G) : R => Character E bv g

      \func of-1 : chi G.ide = R.natCoef lv.len => unfold chi (unfold Character (rewrite (Matrix-of-1, Trace-ide) idp))

      \func Matrix-of-1 : LinearMap.toMatrix lv bv (E.toLinearMap G.ide) = MatrixRing.ide => rewrite (E.toLinearMap-ide, LinearMap.toMatrix_ide) idp
    }