Theorem: IsPrimitiveRoot.sub_one_norm_two' (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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) (ζ - 1) = -2
Tactic:
rw [hζ.eq_neg_one_of_two_right]
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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) (-1 - 1) = -2

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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) (-1 - 1) = -2
Tactic:
suffices Algebra.norm K (algebraMap K L (-2)) = -2 by
  simpa only [sub_eq_add_neg, ← one_add_one_eq_two,
    neg_add_rev, map_add, map_neg, map_one] using this
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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) ((algebraMap K L) (-2)) = -2

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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ (Algebra.norm K) ((algebraMap K L) (-2)) = -2
Tactic:
rw [Algebra.norm_algebraMap, finrank_eq_one_iff'.mpr, pow_one]
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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ ∃ v, v ≠ 0 ∧ ∀ (w : L), ∃ c, c • v = w

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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
⊢ ∃ v, v ≠ 0 ∧ ∀ (w : L), ∃ c, c • v = w
Tactic:
refine ⟨1, one_ne_zero, fun w ↦ ?_⟩
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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
w : L
⊢ ∃ c, c • 1 = w

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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
w : L
⊢ ∃ c, c • 1 = w
Tactic:
simpa only [Algebra.algebraMap_eq_smul_one] using surjective_of_isCyclotomicExtension_two K L w
State after:
no goals

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
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ζ : L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
this : (Algebra.norm K) ((algebraMap K L) (-2)) = -2
⊢ (Algebra.norm K) (-1 - 1) = -2
Tactic:
simpa only [sub_eq_add_neg, ← one_add_one_eq_two,
  neg_add_rev, map_add, map_neg, map_one] using this
State after:
no goals