English
For an Artinian ring R and any module M, the four properties Module.Finite R M, IsNoetherian R M, IsArtinian R M, and IsFiniteLength R M are all equivalent; explicitly, TFAE holds among these four conditions.
Русский
Для Artinian кольца R и любого модуля M эти четыре свойства: Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M эквивалентны между собой.
LaTeX
$$$$\text{IsArtinianRing.tfae: }\operatorname{TFAE}\big([\operatorname{Module.Finite } R M, \operatorname{IsNoetherian } R M, \operatorname{IsArtinian } R M, \operatorname{IsFiniteLength } R M]\big).$$$$
Lean4
theorem tfae [IsArtinianRing R] : List.TFAE [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M] :=
by
tfae_have 2 ↔ 3 := IsSemiprimaryRing.isNoetherian_iff_isArtinian
tfae_have 2 → 1 := fun _ ↦ inferInstance
tfae_have 1 → 3 := fun _ ↦ inferInstance
rw [isFiniteLength_iff_isNoetherian_isArtinian]
tfae_have 4 → 2 := And.left
tfae_have 2 → 4 := fun h ↦ ⟨h, tfae_2_iff_3.mp h⟩
tfae_finish
