Theorem: isCoprime_of_not_zeta_sub_one_dvd (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
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
⊢ IsCoprime (↑↑p) x
Tactic:
letI := IsCyclotomicExtension.numberField {p} ℚ K
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
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ IsCoprime (↑↑p) x

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
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ IsCoprime (↑↑p) x
Tactic:
rwa [← Ideal.isCoprime_span_singleton_iff,
  ← Ideal.span_singleton_eq_span_singleton.mpr (associated_zeta_sub_one_pow_prime hζ),
  ← Ideal.span_singleton_pow, IsCoprime.pow_left_iff, Ideal.isCoprime_iff_gcd,
  hζ.prime_span_sub_one.irreducible.gcd_eq_one_iff, Ideal.dvd_span_singleton,
  Ideal.mem_span_singleton]
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
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ 0 < ↑p - 1

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
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ 0 < ↑p - 1
Tactic:
simpa only [ge_iff_le, tsub_pos_iff_lt] using hpri.out.one_lt
State after:
no goals