Theorem: ne_bot_of_mem_primesOver (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
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
hP' : P = ⊥
⊢ p = ⊥
Tactic:
rw [← hP.2, hP', ← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot]
State after:
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
hP' : P = ⊥
⊢ Function.Injective ⇑(algebraMap R S)

State before:
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
hP' : P = ⊥
⊢ Function.Injective ⇑(algebraMap R S)
Tactic:
exact NoZeroSMulDivisors.algebraMap_injective R S
State after:
no goals