From 815d3cbfa2bf98b4b8f2bcd14819a20eca843e78 Mon Sep 17 00:00:00 2001
From: Antonio Nikishaev
Date: Sun, 5 Apr 2020 02:54:23 +0400
Subject: fix typos in documentation: text

---
 mathcomp/character/integral_char.v | 2 +-
 mathcomp/character/mxabelem.v      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/character')

diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index 7e470b2..2b886a6 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -83,7 +83,7 @@ Qed.
 Section GenericClassSums.
 
 (* This is Isaacs, Theorem (2.4), generalized to an arbitrary field, and with *)
-(* the combinatorial definition of the coeficients exposed.                   *)
+(* the combinatorial definition of the coefficients exposed.                  *)
 (* This part could move to mxrepresentation.*)
 
 Variable (gT : finGroupType) (G : {group gT}) (F : fieldType).
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index 1c3fe0b..92470d9 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -11,7 +11,7 @@ From mathcomp Require Import mxalgebra mxrepresentation.
 (******************************************************************************)
 (*   This file completes the theory developed in mxrepresentation.v with the  *)
 (* construction and properties of linear representations over finite fields,  *)
-(* and in particular the correspondance between internal action on a (normal) *)
+(* and in particular the correspondence between internal action on a (normal) *)
 (* elementary abelian p-subgroup and a linear representation on an Fp-module. *)
 (*   We provide the following next constructions for a finite field F:        *)
 (*        'Zm%act == the action of {unit F} on 'M[F]_(m, n).                  *)
-- 
cgit v1.2.3