diff --git a/library/data/examples/vector.lean b/library/data/examples/vector.lean
index 6f7ef484a..b49b163c1 100644
--- a/library/data/examples/vector.lean
+++ b/library/data/examples/vector.lean
@@ -339,6 +339,6 @@ namespace vector
   | (mk f g l r) n :=
     mk (map f) (map g)
      begin intros, rewrite [map_map, id_of_left_inverse l, map_id], reflexivity end
-     begin intros, rewrite [map_map, id_of_righ_inverse r, map_id], reflexivity end
+     begin intros, rewrite [map_map, id_of_right_inverse r, map_id], reflexivity end
   end
 end vector
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index 6aaf24d02..7db7cb680 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -563,7 +563,7 @@ definition list_equiv_of_equiv {A B : Type} : A ≃ B → list A ≃ list B
 | (mk f g l r) :=
   mk (map f) (map g)
    begin intros, rewrite [map_map, id_of_left_inverse l, map_id], try reflexivity end
-   begin intros, rewrite [map_map, id_of_righ_inverse r, map_id], try reflexivity end
+   begin intros, rewrite [map_map, id_of_right_inverse r, map_id], try reflexivity end
 
 private definition to_nat : list nat → nat
 | []      := 0
diff --git a/library/data/stream.lean b/library/data/stream.lean
index ca616b1ac..4638c89b0 100644
--- a/library/data/stream.lean
+++ b/library/data/stream.lean
@@ -622,7 +622,7 @@ lemma stream_equiv_of_equiv {A B : Type} : A ≃ B → stream A ≃ stream B
 | (mk f g l r) :=
   mk (map f) (map g)
    begin intros, rewrite [map_map, id_of_left_inverse l, map_id] end
-   begin intros, rewrite [map_map, id_of_righ_inverse r, map_id] end
+   begin intros, rewrite [map_map, id_of_right_inverse r, map_id] end
 end
 
 definition lex (rel : A → A → Prop) (s₁ s₂ : stream A) : Prop :=
diff --git a/library/init/function.lean b/library/init/function.lean
index dff86273b..d8acd33dd 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -105,7 +105,7 @@ definition has_left_inverse (f : A → B) : Prop := ∃ finv : B → A, left_inv
 -- g is a right inverse to f
 definition right_inverse (g : B → A) (f : A → B) : Prop := left_inverse f g
 
-definition id_of_righ_inverse {g : B → A} {f : A → B} : right_inverse g f → f ∘ g = id :=
+definition id_of_right_inverse {g : B → A} {f : A → B} : right_inverse g f → f ∘ g = id :=
 assume h, funext h
 
 definition has_right_inverse (f : A → B) : Prop := ∃ finv : B → A, right_inverse finv f