From 8c704cf7eaddd1858113e46ea00a79e094b102db Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Thu, 12 May 2016 15:34:51 +0200 Subject: Fixes doc of mxrepresentation.v --- mathcomp/character/mxrepresentation.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'mathcomp/character/mxrepresentation.v') 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 *) -- cgit v1.2.3