fix(library/init/function): fix typo

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

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

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 :=

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