R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.240355
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
⊢ (if h : Set.Finite (mulSupport fun v => maxPowDividing v I) then ∏ i in Finite.toFinset h, maxPowDividing i I
    else 1) ≠
    0
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.240355
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
rw [Associates.mk_ne_zero, finprod_def]
case inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.240355
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ ∏ v in Finite.toFinset h✝, maxPowDividing v I ≠ 0

case inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.240355
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : ¬Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ 1 ≠ 0
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.240355
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
⊢ (if h : Set.Finite (mulSupport fun v => maxPowDividing v I) then ∏ i in Finite.toFinset h, maxPowDividing i I
    else 1) ≠
    0
split_ifs
case inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.240355
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ ∀ (a : HeightOneSpectrum R), a ∈ Finite.toFinset h✝ → maxPowDividing a I ≠ 0
case inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.240355
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ ∏ v in Finite.toFinset h✝, maxPowDividing v I ≠ 0
rw [Finset.prod_ne_zero_iff]
case inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.240355
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
v : HeightOneSpectrum R
a✝ : v ∈ Finite.toFinset h✝
⊢ maxPowDividing v I ≠ 0
case inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.240355
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ ∀ (a : HeightOneSpectrum R), a ∈ Finite.toFinset h✝ → maxPowDividing a I ≠ 0
intro v _
no goals
case inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.240355
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
v : HeightOneSpectrum R
a✝ : v ∈ Finite.toFinset h✝
⊢ maxPowDividing v I ≠ 0
apply pow_ne_zero _ v.ne_bot
no goals
case inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.240355
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : ¬Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ 1 ≠ 0
exact one_ne_zero