aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/fingraph.v
diff options
context:
space:
mode:
authoraffeldt-aist2020-04-09 13:43:32 +0200
committerGitHub2020-04-09 13:43:32 +0200
commitad82c5fb56113bdef57e96f6a79000a29803eb38 (patch)
tree07c9348f97482124e7a19725863dd3373ea598e5 /mathcomp/ssreflect/fingraph.v
parent504a34ba48a29a252c40cfc0467f6b192243b6bc (diff)
parent31dec18a2539cfdac70fd87401db2b4b14d81d16 (diff)
Merge pull request #474 from llelf/doc-typos
Documentation typos
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} : [<->