Theorem: exists_zeta_sub_one_dvd_sub_Int (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
a : 𝓞 K
⊢ ∃ b, ↑hζ.unit' - 1 ∣ a - ↑b
Tactic:
letI : AddGroup (𝓞 K ⧸ Ideal.span (singleton (hζ.unit' - 1: 𝓞 K))) := inferInstance
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
a : 𝓞 K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ∃ b, ↑hζ.unit' - 1 ∣ a - ↑b

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
a : 𝓞 K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ∃ b, ↑hζ.unit' - 1 ∣ a - ↑b
Tactic:
letI : Fact (Nat.Prime p) := hpri
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
⊢ ∃ b, ↑hζ.unit' - 1 ∣ a - ↑b

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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
⊢ ∃ b, ↑hζ.unit' - 1 ∣ a - ↑b
Tactic:
simp_rw [← Ideal.Quotient.eq_zero_iff_dvd, map_sub, sub_eq_zero, ← SModEq.Ideal_def]
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
⊢ ∃ b, a ≡ ↑b [SMOD Ideal.span {↑hζ.unit' - 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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
⊢ ∃ b, a ≡ ↑b [SMOD Ideal.span {↑hζ.unit' - 1}]
Tactic:
convert exists_int_sModEq hζ.subOneIntegralPowerBasis' a
State after:
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ↑hζ.unit' - 1 = hζ.subOneIntegralPowerBasis'.gen

State before:
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ↑hζ.unit' - 1 = hζ.subOneIntegralPowerBasis'.gen
Tactic:
rw [hζ.subOneIntegralPowerBasis'_gen]
State after:
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ↑hζ.unit' - 1 = hζ.toInteger - 1

State before:
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ↑hζ.unit' - 1 = hζ.toInteger - 1
Tactic:
rw [Subtype.ext_iff, AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one]
State after:
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ζ - 1 = ↑(hζ.toInteger - 1)

State before:
case h.e'_2.h.h.e'_6.h.e'_3.h.e'_4
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
a : 𝓞 K
this✝ : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
this : Fact (↑p).Prime := hpri
x✝ : ℤ
⊢ ζ - 1 = ↑(hζ.toInteger - 1)
Tactic:
rfl
State after:
no goals