aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/fingraph.v
diff options
context:
space:
mode:
authorAntonio Nikishaev2020-04-05 02:54:23 +0400
committerAntonio Nikishaev2020-04-08 01:13:13 +0400
commit815d3cbfa2bf98b4b8f2bcd14819a20eca843e78 (patch)
treed3564d7ccb62b38493fde1a0fc23ff94410074ec /mathcomp/ssreflect/fingraph.v
parent14e28e78155e3e6cfbe78aee0964569283f04d7d (diff)
fix typos in documentation: text
Diffstat (limited to 'mathcomp/ssreflect/fingraph.v')
-rw-r--r--mathcomp/ssreflect/fingraph.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index afd43df..09ca95f 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -776,7 +776,7 @@ Qed.
(* has to apply it to the natural numbers corresponding to the line, e.g. *)
(* `orbitPcycle 0 2 : fcycle f (orbit x) <-> exists k, iter k.+1 f x = x`. *)
(* examples of this are in order_id_cycle and fconnnect_f. *)
-(* One may also use lemma all_iffLR to get a one sided impliciation, as in *)
+(* One may also use lemma all_iffLR to get a one sided implication, as in *)
(* orderPcycle. *)
(*****************************************************************************)
Lemma orbitPcycle {x} : [<->