Theorem: Ideal.spanIntNorm_bot (FltRegular/NumberTheory/IdealNorm.lean)

State before:
R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : IsIntegrallyClosed R
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : IsSeparable (FractionRing R) (FractionRing S)
inst✝² : Nontrivial S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
x : R
hx : x ∈ ⇑(Algebra.intNorm R S) '' ↑⊥
⊢ x = 0
Tactic:
simpa using hx
State after:
no goals