aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorCyril Cohen2019-10-15 12:36:10 +0200
committerGitHub2019-10-15 12:36:10 +0200
commitba5ad832912004b5f54bcef9b6d5916b7ca876ba (patch)
treeb34d62c0d92d653e39250ffbce863b6f7f8f16ae
parent5d963c6ae75cce78b7107180d57b456e37b00728 (diff)
parente48f266b9f2418a619fc1217250fd2942854dcbe (diff)
Merge pull request #390 from thery/doc
typo in ssralg
-rw-r--r--mathcomp/algebra/ssralg.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index d35253c..486b12e 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -94,7 +94,7 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
(* GRing.rreg x <-> x if right-regular, i.e., *%R x is injective. *)
(* [char R] == the characteristic of R, defined as the set of *)
(* prime numbers p such that p%:R = 0 in R. The set *)
-(* [char p] has a most one element, and is *)
+(* [char R] has at most one element, and is *)
(* implemented as a pred_nat collective predicate *)
(* (see prime.v); thus the statement p \in [char R] *)
(* can be read as `R has characteristic p', while *)