Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit f318e5d

Browse files
committed
chore(ring_theory/artinian): typo (#9140)
1 parent 579ca5e commit f318e5d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/ring_theory/artinian.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -187,7 +187,7 @@ end
187187

188188
/-- A module is Artinian iff every nonempty set of submodules has a minimal submodule among them.
189189
-/
190-
theorem set_has_minimal_iff_artinrian :
190+
theorem set_has_minimal_iff_artinian :
191191
(∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, I ≤ M' → I = M') ↔
192192
is_artinian R M :=
193193
by rw [is_artinian_iff_well_founded, well_founded.well_founded_iff_has_min']

0 commit comments

Comments
 (0)