chore(ring_theory): typo fix (#9067)

`principal_idea_ring` -> `principal_ideal_ring`
leanprover-community · Sep 7, 2021 · 9c886ff · 9c886ff
1 parent f8cfed4
commit 9c886ff
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ring_theory/principal_ideal_domain.lean b/src/ring_theory/principal_ideal_domain.lean
@@ -56,7 +56,7 @@ class is_principal_ideal_ring (R : Type u) [ring R] : Prop :=
 attribute [instance] is_principal_ideal_ring.principal
 
 @[priority 100]
-instance division_ring.is_principal_idea_ring (K : Type u) [division_ring K] :
+instance division_ring.is_principal_ideal_ring (K : Type u) [division_ring K] :
   is_principal_ideal_ring K :=
 { principal := λ S, by rcases ideal.eq_bot_or_top S with (rfl|rfl); apply_instance }