Theorem: primesOverFinset_bot (FltRegular/NumberTheory/GaloisPrime.lean)

State before:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsDedekindDomain S
⊢ primesOverFinset S ⊥ = ∅
Tactic:
classical
rw [primesOverFinset, Ideal.map_bot, ← Ideal.zero_eq_bot, factors_zero]
rfl
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsDedekindDomain S
⊢ primesOverFinset S ⊥ = ∅
Tactic:
rw [primesOverFinset, Ideal.map_bot, ← Ideal.zero_eq_bot, factors_zero]
State after:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsDedekindDomain S
⊢ Multiset.toFinset 0 = ∅

State before:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsDedekindDomain S
⊢ Multiset.toFinset 0 = ∅
Tactic:
rfl
State after:
no goals