fix(principal_ideal_domain): correct spelling mistake (#582)

leanprover-community · Jan 10, 2019 · b1684fe · b1684fe
1 parent 6e97721
commit b1684fe
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/ring_theory/principal_ideal_domain.lean b/ring_theory/principal_ideal_domain.lean
@@ -131,7 +131,7 @@ lemma irreducible_iff_prime {p : α} : irreducible p ↔ prime p :=
     (is_maximal_of_irreducible hp).is_prime,
   irreducible_of_prime⟩
 
-lemma associates_iredducible_iff_prime : ∀{p : associates α}, irreducible p ↔ p.prime :=
+lemma associates_irreducible_iff_prime : ∀{p : associates α}, irreducible p ↔ p.prime :=
 associates.forall_associated.2 $ assume a,
 by rw [associates.irreducible_mk_iff, associates.prime_mk, irreducible_iff_prime]