Theorem: IsPrimitiveRoot.p_mem_one_sub_zeta (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
classical
have key : _ = (p : 𝓞 K) := @Polynomial.eval_one_cyclotomic_prime _ _ _ hp
rw [cyclotomic_eq_prod_X_sub_primitiveRoots hζ.unit'_coe, eval_prod] at key
simp only [eval_sub, eval_X, eval_C] at key
have : {↑hζ.unit'} ⊆ primitiveRoots p (𝓞 K) := by simpa using hζ.unit'_coe
rw [← Finset.prod_sdiff this, Finset.prod_singleton] at key
rw [← key]
have := (Ideal.neg_mem_iff I).mpr (Ideal.subset_span (Set.mem_singleton ζ1))
rw [neg_sub] at this
exact Ideal.mul_mem_left _ _ this
State after:
no goals

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
have key : _ = (p : 𝓞 K) := @Polynomial.eval_one_cyclotomic_prime _ _ _ hp
State after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : eval 1 (cyclotomic (↑p) (𝓞 K)) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : eval 1 (cyclotomic (↑p) (𝓞 K)) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [cyclotomic_eq_prod_X_sub_primitiveRoots hζ.unit'_coe, eval_prod] at key
State after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ j ∈ primitiveRoots (↑p) (𝓞 K), eval 1 (X - C j) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ j ∈ primitiveRoots (↑p) (𝓞 K), eval 1 (X - C j) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
simp only [eval_sub, eval_X, eval_C] at key
State after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x) = ↑↑p
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
have : {↑hζ.unit'} ⊆ primitiveRoots p (𝓞 K) := by simpa using hζ.unit'_coe
State after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x) = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x) = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [← Finset.prod_sdiff this, Finset.prod_singleton] at key
State after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [← key]
State after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
have := (Ideal.neg_mem_iff I).mpr (Ideal.subset_span (Set.mem_singleton ζ1))
State after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this✝ : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
this : -(↑hζ.unit' - 1) ∈ Ideal.span {↑hζ.unit' - 1}
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this✝ : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
this : -(↑hζ.unit' - 1) ∈ Ideal.span {↑hζ.unit' - 1}
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [neg_sub] at this
State after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this✝ : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
this : 1 - ↑hζ.unit' ∈ Ideal.span {↑hζ.unit' - 1}
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') = ↑↑p
this✝ : {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
this : 1 - ↑hζ.unit' ∈ Ideal.span {↑hζ.unit' - 1}
⊢ (∏ x ∈ primitiveRoots (↑p) (𝓞 K) \ {↑hζ.unit'}, (1 - x)) * (1 - ↑hζ.unit') ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
exact Ideal.mul_mem_left _ _ this
State after:
no goals

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
hp : Fact (↑p).Prime
key : ∏ x ∈ primitiveRoots (↑p) (𝓞 K), (1 - x) = ↑↑p
⊢ {↑hζ.unit'} ⊆ primitiveRoots (↑p) (𝓞 K)
Tactic:
simpa using hζ.unit'_coe
State after:
no goals