diff options
| author | Florent Hivert | 2016-05-12 15:34:51 +0200 |
|---|---|---|
| committer | Florent Hivert | 2016-05-12 15:34:51 +0200 |
| commit | 8c704cf7eaddd1858113e46ea00a79e094b102db (patch) | |
| tree | 155a1642e93f4b2956daa380616dc37e3c39448f | |
| parent | 0fedd37679abe2a9909ec03aebf01aab359a06fd (diff) | |
Fixes doc of mxrepresentation.v
| -rw-r--r-- | mathcomp/character/mxrepresentation.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index b270df0..7eef614 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -47,7 +47,7 @@ Require Import commutator cyclic center pgroup matrix mxalgebra mxpoly. (* with the square matrix A. *) (* rcenter rG == the subgroup of G whose representation via rG consists of *) (* scalar matrices. *) -(* mxcentg rG f <=> f commutes with every matrix in the representation of G *) +(* centgmx rG f <=> f commutes with every matrix in the representation of G *) (* (i.e., f is a total rG-homomorphism). *) (* rstab rG U == the subgroup of G whose representation via r fixes all *) (* vectors in U, pointwise. *) @@ -182,7 +182,7 @@ Require Import commutator cyclic center pgroup matrix mxalgebra mxpoly. (* irr_mode i z == the unique eigenvalue of irr_repr i z, at least when *) (* irr_repr i z is scalar (e.g., when z \in 'Z(G)). *) (* [1 sG]%irr == the index of the principal representation of G, in *) -(* sG : irrType F G. The i argument ot irr_repr, irr_degree *) +(* sG : irrType F G. The i argument of irr_repr, irr_degree *) (* and irr_mode is in the %irr scope. This notation may be *) (* replaced locally by an interpretation of 1%irr as [1 sG] *) (* for some specific irrType sG. *) @@ -233,7 +233,7 @@ Require Import commutator cyclic center pgroup matrix mxalgebra mxpoly. (* much better suited to our needs. *) (* Here are the main definitions of MatrixGenField; they all have three *) (* proofs as arguments: rG : mx_repr r G, irrG : mx_irreducible rG, and *) -(* cGA : mxcentg rG A, which ensure the validity of the construction and *) +(* cGA : centgmx rG A, which ensure the validity of the construction and *) (* allow us to define Canonical instances (the ~~ is_scalar_mx A assumption *) (* is only needed to prove reducibility). *) (* + gen_of irrG cGA == the carrier type of the field generated by A. It is *) |