Theorem: IsPrimitiveRoot.cyclotomic_eq_minpoly (FltRegular/NumberTheory/CyclotomicRing.lean)

State before:
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ minpoly ℤ x = cyclotomic p ℤ
Tactic:
apply Polynomial.map_injective (algebraMap ℤ ℚ) (RingHom.injective_int (algebraMap ℤ ℚ))
State after:
case a
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ map (algebraMap ℤ ℚ) (minpoly ℤ x) = map (algebraMap ℤ ℚ) (cyclotomic p ℤ)

State before:
case a
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ map (algebraMap ℤ ℚ) (minpoly ℤ x) = map (algebraMap ℤ ℚ) (cyclotomic p ℤ)
Tactic:
rw [← minpoly.isIntegrallyClosed_eq_field_fractions ℚ (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ),
  ← cyclotomic_eq_minpoly_rat (n := p), map_cyclotomic]
State after:
case a.h
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ IsPrimitiveRoot ((algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) x) p

case a.hpos
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ 0 < p

case a
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ IsIntegral ℤ x

State before:
case a.h
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ IsPrimitiveRoot ((algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) x) p
Tactic:
exact hx
State after:
no goals

State before:
case a.hpos
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ 0 < p
Tactic:
exact hpri.out.pos
State after:
no goals

State before:
case a
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ IsIntegral ℤ x
Tactic:
exact IsIntegralClosure.isIntegral _ (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ) _
State after:
no goals