Theorem: associated_zeta_sub_one_pow_prime (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
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) ↑↑p
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
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) ↑↑p

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
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) ↑↑p
Tactic:
haveI : 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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) ↑↑p

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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) ↑↑p
Tactic:
rw [← eval_one_cyclotomic_prime (R := 𝓞 K) (p := p),
  cyclotomic_eq_prod_X_sub_primitiveRoots hζ.unit'_coe, eval_prod]
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) (∏ j ∈ primitiveRoots (↑p) (𝓞 K), eval 1 (X - C j))

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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) (∏ j ∈ primitiveRoots (↑p) (𝓞 K), eval 1 (X - C j))
Tactic:
simp only [eval_sub, eval_X, eval_C]
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) (∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - 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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated ((↑hζ.unit' - 1) ^ (↑p - 1)) (∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x))
Tactic:
rw [← Nat.totient_prime this.out, ← hζ.unit'_coe.card_primitiveRoots, ← Finset.prod_const]
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated (∏ _x ∈ primitiveRoots (↑p) (𝓞 K), (↑hζ.unit' - 1)) (∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - 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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ Associated (∏ _x ∈ primitiveRoots (↑p) (𝓞 K), (↑hζ.unit' - 1)) (∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x))
Tactic:
apply Associated.prod
State after:
case h
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ ∀ i ∈ primitiveRoots (↑p) (𝓞 K), Associated (↑hζ.unit' - 1) (1 - i)

State before:
case h
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ ∀ i ∈ primitiveRoots (↑p) (𝓞 K), Associated (↑hζ.unit' - 1) (1 - i)
Tactic:
intro η hη
State after:
case h
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
η : 𝓞 K
hη : η ∈ primitiveRoots (↑p) (𝓞 K)
⊢ Associated (↑hζ.unit' - 1) (1 - η)

State before:
case h
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
η : 𝓞 K
hη : η ∈ primitiveRoots (↑p) (𝓞 K)
⊢ Associated (↑hζ.unit' - 1) (1 - η)
Tactic:
exact hζ.unit'_coe.associated_sub_one hpri.out
  (one_mem_nthRootsFinset this.out.pos)
  ((isPrimitiveRoot_of_mem_primitiveRoots hη).mem_nthRootsFinset hpri.out.pos)
    ((isPrimitiveRoot_of_mem_primitiveRoots hη).ne_one hpri.out.one_lt).symm
State after:
no goals