[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
classical exact isPrincipal_of_FG (Ideal.span { x, y }) ⟨{ x, y }, by simp⟩
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
exact isPrincipal_of_FG (Ideal.span { x, y }) ⟨{ x, y }, by simp⟩
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ Ideal.span ↑{x, y} = Ideal.span {x, y}
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
classical
constructor
· intro H x y; infer_instance
· intro H
  constructor
  apply Submodule.fg_induction
  · exact fun _ => ⟨⟨_, rfl⟩⟩
  · rintro _ _ ⟨⟨x, rfl⟩⟩ ⟨⟨y, rfl⟩⟩; rw [← Submodule.span_insert]; exact H _ _
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
inst✝ : CommRing R
⊢ IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
intro H x y
[GOAL]
case mp
R : Type u
inst✝ : CommRing R
H : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
R : Type u
inst✝ : CommRing R
⊢ (∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})) → IsBezout R
[PROOFSTEP]
intro H
[GOAL]
case mpr
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ IsBezout R
[PROOFSTEP]
constructor
[GOAL]
case mpr.isPrincipal_of_FG
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (I : Ideal R), Ideal.FG I → Submodule.IsPrincipal I
[PROOFSTEP]
apply Submodule.fg_induction
[GOAL]
case mpr.isPrincipal_of_FG.h₁
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (x : R), Submodule.IsPrincipal (Submodule.span R {x})
[PROOFSTEP]
exact fun _ => ⟨⟨_, rfl⟩⟩
[GOAL]
case mpr.isPrincipal_of_FG.h₂
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (M₁ M₂ : Submodule R R), Submodule.IsPrincipal M₁ → Submodule.IsPrincipal M₂ → Submodule.IsPrincipal (M₁ ⊔ M₂)
[PROOFSTEP]
rintro _ _ ⟨⟨x, rfl⟩⟩ ⟨⟨y, rfl⟩⟩
[GOAL]
case mpr.isPrincipal_of_FG.h₂.mk.intro.mk.intro
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
x y : R
⊢ Submodule.IsPrincipal (Submodule.span R {x} ⊔ Submodule.span R {y})
[PROOFSTEP]
rw [← Submodule.span_insert]
[GOAL]
case mpr.isPrincipal_of_FG.h₂.mk.intro.mk.intro
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
x y : R
⊢ Submodule.IsPrincipal (Submodule.span R {x, y})
[PROOFSTEP]
exact H _ _
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ x ∈ {x, y}
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ y ∈ {x, y}
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y z : R
hx : z ∣ x
hy : z ∣ y
⊢ z ∣ gcd x y
[PROOFSTEP]
rw [← Ideal.span_singleton_le_span_singleton] at hx hy ⊢
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y z : R
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {gcd x y} ≤ Ideal.span {z}
[PROOFSTEP]
rw [span_gcd, Ideal.span_insert, sup_le_iff]
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y z : R
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {x} ≤ Ideal.span {z} ∧ Ideal.span {y} ≤ Ideal.span {z}
[PROOFSTEP]
exact ⟨hx, hy⟩
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ gcd x y ∈ Ideal.span {x, y}
[PROOFSTEP]
rw [← span_gcd]
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ gcd x y ∈ Ideal.span {gcd x y}
[PROOFSTEP]
apply Ideal.subset_span
[GOAL]
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ gcd x y ∈ {gcd x y}
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsBezout R
⊢ IsIntegrallyClosed R
[PROOFSTEP]
classical exact GCDMonoid.toIsIntegrallyClosed
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsBezout R
⊢ IsIntegrallyClosed R
[PROOFSTEP]
exact GCDMonoid.toIsIntegrallyClosed
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
⊢ IsBezout S
[PROOFSTEP]
rw [iff_span_pair_isPrincipal]
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
⊢ ∀ (x y : S), Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
intro x y
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : S
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
[PROOFSTEP]
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := hf x, hf y
[GOAL]
case intro.intro
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {↑f x, ↑f y})
[PROOFSTEP]
use f (gcd x y)
[GOAL]
case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f x, ↑f y} = Submodule.span S {↑f (gcd x y)}
[PROOFSTEP]
trans Ideal.map f (Ideal.span {gcd x y})
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f x, ↑f y} = Ideal.map f (Ideal.span {gcd x y})
[PROOFSTEP]
rw [span_gcd, Ideal.map_span, Set.image_insert_eq, Set.image_singleton]
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.map f (Ideal.span {gcd x y}) = Submodule.span S {↑f (gcd x y)}
[PROOFSTEP]
rw [Ideal.map_span, Set.image_singleton]
[GOAL]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f (gcd x y)} = Submodule.span S {↑f (gcd x y)}
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
classical
tfae_have 1 → 2
· intro H; exact ⟨fun I => isPrincipal_of_FG _ (IsNoetherian.noetherian _)⟩
tfae_have 2 → 3
· intro; infer_instance
tfae_have 3 → 4
· intro; infer_instance
tfae_have 4 → 1
· rintro ⟨h⟩
  rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded]
  apply RelEmbedding.wellFounded _ h
  have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span { x } := fun ⟨I, hI⟩ =>
    (IsBezout.isPrincipal_of_FG I hI).1
  choose f hf using this
  exact
    { toFun := f
      inj' := fun x y e => by ext1; rw [hf, hf, e]
      map_rel_iff' := by
        dsimp
        intro a b
        rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
        rfl }
tfae_finish
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
⊢ IsNoetherianRing R → IsPrincipalIdealRing R
[PROOFSTEP]
intro H
[GOAL]
case tfae_1_to_2
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
H : IsNoetherianRing R
⊢ IsPrincipalIdealRing R
[PROOFSTEP]
exact ⟨fun I => isPrincipal_of_FG _ (IsNoetherian.noetherian _)⟩
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
tfae_have 2 → 3
[GOAL]
case tfae_2_to_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
⊢ IsPrincipalIdealRing R → UniqueFactorizationMonoid R
[PROOFSTEP]
intro
[GOAL]
case tfae_2_to_3
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
✝ : IsPrincipalIdealRing R
⊢ UniqueFactorizationMonoid R
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
tfae_have 3 → 4
[GOAL]
case tfae_3_to_4
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
⊢ UniqueFactorizationMonoid R → WfDvdMonoid R
[PROOFSTEP]
intro
[GOAL]
case tfae_3_to_4
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
✝ : UniqueFactorizationMonoid R
⊢ WfDvdMonoid R
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
tfae_have 4 → 1
[GOAL]
case tfae_4_to_1
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
⊢ WfDvdMonoid R → IsNoetherianRing R
[PROOFSTEP]
rintro ⟨h⟩
[GOAL]
case tfae_4_to_1.mk
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
⊢ IsNoetherianRing R
[PROOFSTEP]
rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded]
[GOAL]
case tfae_4_to_1.mk
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
apply RelEmbedding.wellFounded _ h
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
⊢ (fun x x_1 => x > x_1) ↪r DvdNotUnit
[PROOFSTEP]
have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span { x } := fun ⟨I, hI⟩ =>
  (IsBezout.isPrincipal_of_FG I hI).1
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
this : ∀ (I : { J // Ideal.FG J }), ∃ x, ↑I = Ideal.span {x}
⊢ (fun x x_1 => x > x_1) ↪r DvdNotUnit
[PROOFSTEP]
choose f hf using this
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
⊢ (fun x x_1 => x > x_1) ↪r DvdNotUnit
[PROOFSTEP]
exact
  { toFun := f
    inj' := fun x y e => by ext1; rw [hf, hf, e]
    map_rel_iff' := by
      dsimp
      intro a b
      rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
      rfl }
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
x y : { N // Submodule.FG N }
e : f x = f y
⊢ x = y
[PROOFSTEP]
ext1
[GOAL]
case a
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
x y : { N // Submodule.FG N }
e : f x = f y
⊢ ↑x = ↑y
[PROOFSTEP]
rw [hf, hf, e]
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
⊢ ∀ {a b : { N // Submodule.FG N }},
    DvdNotUnit (↑{ toFun := f, inj' := (_ : ∀ (x y : { N // Submodule.FG N }), f x = f y → x = y) } a)
        (↑{ toFun := f, inj' := (_ : ∀ (x y : { N // Submodule.FG N }), f x = f y → x = y) } b) ↔
      a > b
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
⊢ ∀ {a b : { N // Submodule.FG N }}, DvdNotUnit (f a) (f b) ↔ a > b
[PROOFSTEP]
intro a b
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
a b : { N // Submodule.FG N }
⊢ DvdNotUnit (f a) (f b) ↔ a > b
[PROOFSTEP]
rw [← Ideal.span_singleton_lt_span_singleton, ← hf, ← hf]
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
h : WellFounded DvdNotUnit
f : { J // Ideal.FG J } → R
hf : ∀ (I : { J // Ideal.FG J }), ↑I = Ideal.span {f I}
a b : { N // Submodule.FG N }
⊢ ↑b < ↑a ↔ a > b
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
tfae_1_to_2 : IsNoetherianRing R → IsPrincipalIdealRing R
tfae_2_to_3 : IsPrincipalIdealRing R → UniqueFactorizationMonoid R
tfae_3_to_4 : UniqueFactorizationMonoid R → WfDvdMonoid R
tfae_4_to_1 : WfDvdMonoid R → IsNoetherianRing R
⊢ List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]
[PROOFSTEP]
tfae_finish
