From 9cd7db3feac878596ce656824e7617aed6922f9a Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 25 Jul 2015 12:32:04 -0400 Subject: [PATCH] fix(library/data/list/perm): fix typo in theorem names --- library/data/list/perm.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 775428a458..59e7ccad55 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -119,7 +119,7 @@ assume p, perm.induction_on p (λ x y l, by rewrite *length_cons) (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, eq.trans r₁ r₂) -theorem eq_singlenton_of_perm_inv (a : A) {l : list A} : [a] ~ l → l = [a] := +theorem eq_singleton_of_perm_inv (a : A) {l : list A} : [a] ~ l → l = [a] := have gen : ∀ l₂, perm l₂ l → l₂ = [a] → l = [a], from take l₂, assume p, perm.induction_on p (λ e, e) @@ -134,10 +134,10 @@ have gen : ∀ l₂, perm l₂ l → l₂ = [a] → l = [a], from (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂ e, r₂ (r₁ e)), assume p, gen [a] p rfl -theorem eq_singlenton_of_perm (a b : A) : [a] ~ [b] → a = b := +theorem eq_singleton_of_perm (a b : A) : [a] ~ [b] → a = b := assume p, begin - injection eq_singlenton_of_perm_inv a p with e₁, + injection eq_singleton_of_perm_inv a p with e₁, rewrite e₁ end