diff options
| author | Antonio Nikishaev | 2020-04-09 10:54:37 +0400 |
|---|---|---|
| committer | Antonio Nikishaev | 2020-04-09 10:54:37 +0400 |
| commit | 7d6e46ec9c8067553e9a82b5345778f00cf3c1e9 (patch) | |
| tree | 74ce40f12464d89c103250f529659f01a32cd253 | |
| parent | 52e091587f9fa65f6184ae5e4c6b63677281376b (diff) | |
more typos
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 6832ea7..12b0601 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -437,7 +437,7 @@ End Endo. Variable aT : Type. -(* The invariant of an function f wrt a projection k is the pred of points *) +(* The invariant of a function f wrt a projection k is the pred of points *) (* that have the same projection as their image. *) Definition invariant (rT : eqType) f (k : aT -> rT) := |