Theorem: norm_dvd_iff (FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Infinite R
inst✝¹ : Module.Free ℤ R
inst✝ : Module.Finite ℤ R
x : R
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Algebra.norm ℤ) x ∣ y ↔ x ∣ ↑y
Tactic:
rw [← Ideal.mem_span_singleton (y := x), ← eq_intCast (algebraMap ℤ R), ← Ideal.mem_comap,
  ← Ideal.span_singleton_absNorm, Ideal.mem_span_singleton, Ideal.absNorm_span_singleton,
  Int.natAbs_dvd]
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Infinite R
inst✝¹ : Module.Free ℤ R
inst✝ : Module.Finite ℤ R
x : R
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Ideal.absNorm (Ideal.span {x})).Prime

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Infinite R
inst✝¹ : Module.Free ℤ R
inst✝ : Module.Finite ℤ R
x : R
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Ideal.absNorm (Ideal.span {x})).Prime
Tactic:
rwa [Ideal.absNorm_span_singleton, ← Int.prime_iff_natAbs_prime]
State after:
no goals