-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem norm_eq_one [IsDomain L] [IsCyclotomicExtension {n} K L] (hn : n ≠ 2)
    (hirr : Irreducible (cyclotomic n K)) : norm K ζ = 1

Proof state:
case pos
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : ζ = 1
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : n = 1
⊢ (Algebra.norm K) ζ = 1

Tactic:
rw [hζ, show 1 = algebraMap K L 1 by simp, Algebra.norm_algebraMap, one_pow]

Result:
no goals

Proof state:
case neg
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : 2 ≤ n
⊢ (-1) ^ φ ↑n = 1

Tactic:
exact (totient_even <| h1.lt_of_ne hn.symm).neg_one_pow

Result:
no goals

Proof state:
case neg
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : 2 ≤ n
⊢ (Algebra.norm K) ζ = 1

Tactic:
rw [← hζ.powerBasis_gen K, PowerBasis.norm_gen_eq_coeff_zero_minpoly, hζ.powerBasis_gen K, ←
  hζ.minpoly_eq_cyclotomic_of_irreducible hirr,
  (cyclotomic_coeff_zero K h1 : coeff (cyclotomic n K) 0 = 1), mul_one,
  hζ.powerBasis_dim K, ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, natDegree_cyclotomic]

Result:
case neg
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : 2 ≤ n
⊢ (-1) ^ φ ↑n = 1

Proof state:
case neg
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : ¬n = 1
⊢ (Algebra.norm K) ζ = 1

Tactic:
replace h1 : 2 ≤ n := by
  by_contra! h
  exact h1 (PNat.eq_one_of_lt_two h)

Result:
case neg
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : 2 ≤ n
⊢ (Algebra.norm K) ζ = 1

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
⊢ (Algebra.norm K) ζ = 1

Tactic:
by_cases h1 : n = 1

Result:
case pos
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : n = 1
⊢ (Algebra.norm K) ζ = 1

case neg
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : ¬n = 1
⊢ (Algebra.norm K) ζ = 1

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : ¬n = 1
⊢ 2 ≤ n

Tactic:
by_contra! h

Result:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : ¬n = 1
h : n < 2
⊢ False

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
⊢ (Algebra.norm K) ζ = 1

Tactic:
haveI := IsCyclotomicExtension.neZero' n K L

Result:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
⊢ (Algebra.norm K) ζ = 1

Proof state:
case pos
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : n = 1
⊢ (Algebra.norm K) ζ = 1

Tactic:
rw [h1, one_coe, one_right_iff] at hζ

Result:
case pos
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : ζ = 1
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : n = 1
⊢ (Algebra.norm K) ζ = 1

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : ζ = 1
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : n = 1
⊢ 1 = (algebraMap K L) 1

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
h1 : ¬n = 1
h : n < 2
⊢ False

Tactic:
exact h1 (PNat.eq_one_of_lt_two h)

Result:
no goals