Theorem: CyclotomicIntegers.nontrivial (FltRegular/NumberTheory/CyclotomicRing.lean)

State before:
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
⊢ Nontrivial (CyclotomicIntegers p)
Tactic:
apply Ideal.Quotient.nontrivial
State after:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
⊢ Ideal.span {cyclotomic p ℤ} ≠ ⊤

State before:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
⊢ Ideal.span {cyclotomic p ℤ} ≠ ⊤
Tactic:
simp only [ne_eq, Ideal.span_singleton_eq_top]
State after:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
⊢ ¬IsUnit (cyclotomic p ℤ)

State before:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
⊢ ¬IsUnit (cyclotomic p ℤ)
Tactic:
intro h
State after:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
h : IsUnit (cyclotomic p ℤ)
⊢ False

State before:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
h : IsUnit (cyclotomic p ℤ)
⊢ False
Tactic:
have := natDegree_eq_zero_of_isUnit h
State after:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
h : IsUnit (cyclotomic p ℤ)
this : (cyclotomic p ℤ).natDegree = 0
⊢ False

State before:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
h : IsUnit (cyclotomic p ℤ)
this : (cyclotomic p ℤ).natDegree = 0
⊢ False
Tactic:
rw [natDegree_cyclotomic] at this
State after:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
h : IsUnit (cyclotomic p ℤ)
this : p.totient = 0
⊢ False

State before:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
h : IsUnit (cyclotomic p ℤ)
this : p.totient = 0
⊢ False
Tactic:
exact this.not_gt (Nat.totient_pos.2 <| Nat.zero_lt_of_ne_zero hp)
State after:
no goals