From c1b0ed734dc4ce23d9ac9233c24a7c415e2e21b4 Mon Sep 17 00:00:00 2001
From: thery
Date: Thu, 14 Nov 2019 17:22:01 +0100
Subject: typo

---
 mathcomp/algebra/ssralg.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/algebra')

diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 88920e0..f385ad5 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -409,7 +409,7 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
 (*  [rmorphism of f as g] == an f-clone of the rmorphism structure of g.      *)
 (*       [rmorphism of f] == a clone of an existing additive structure on f.  *)
 (*  -> If R and S are UnitRings the f also maps units to units and inverses   *)
-(*     of units to inverses; if R is a field then f if a field isomorphism    *)
+(*     of units to inverses; if R is a field then f is a field isomorphism    *)
 (*     between R and its image.                                               *)
 (*  -> As rmorphism coerces to both additive and multiplicative, all          *)
 (*     structures for f can be built from a single proof of rmorphism f.      *)
-- 
cgit v1.2.3