case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
⊢ Submodule.IsPrincipal ⊥

case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ Submodule.IsPrincipal I
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
⊢ Submodule.IsPrincipal I
obtain rfl | hI := eq_or_ne I ⊥
case inr.hf
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ Set.Finite {I | IsMaximal I}

case inr.hI
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ IsUnit ↑I
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ Submodule.IsPrincipal I
apply Ideal.IsPrincipal.of_finite_maximals_of_isUnit
no goals
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
⊢ Submodule.IsPrincipal ⊥
exact bot_isPrincipal
case inr.hf
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ {I | IsMaximal I} ⊆ {I | IsPrime I}
case inr.hf
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ Set.Finite {I | IsMaximal I}
apply h.subset
no goals
case inr.hf
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ {I | IsMaximal I} ⊆ {I | IsPrime I}
exact @Ideal.IsMaximal.isPrime _ _
no goals
case inr.hI
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
h : Set.Finite {I | IsPrime I}
I : Ideal R
hI : I ≠ ⊥
⊢ IsUnit ↑I
exact isUnit_of_mul_eq_one _ _ (FractionalIdeal.coe_ideal_mul_inv I hI)