internlm/Lean-Github huggingface dataset:
Theorem: IsPrimitiveRoot.cyclotomic_eq_minpoly
Proof 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 ℤ ℚ))
Proof state after:
case a
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ map (algebraMap ℤ ℚ) (minpoly ℤ x) = map (algebraMap ℤ ℚ) (cyclotomic p ℤ)
Theorem: IsPrimitiveRoot.cyclotomic_eq_minpoly
Proof 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]
Proof 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
Theorem: IsPrimitiveRoot.cyclotomic_eq_minpoly
Proof 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
Proof state after:
no goals
Theorem: IsPrimitiveRoot.cyclotomic_eq_minpoly
Proof state before:
case a.hpos
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ 0 < p
Tactic:
exact hpri.out.pos
Proof state after:
no goals
Theorem: IsPrimitiveRoot.cyclotomic_eq_minpoly
Proof 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⟩ ℚ) _
Proof state after:
no goals
Theorem: AdjoinRoot.aeval_root
Proof state before:
p : ℕ
hpri : Fact p.Prime
R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ (aeval (root P)) P = 0
Tactic:
simp
Proof state after:
no goals
Theorem: CyclotomicIntegers.equiv_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ (equiv p) (zeta p) = ⋯.toInteger
Tactic:
letI p' : ℕ+ := ⟨p, hpri.out.pos⟩
Proof state after:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
⊢ (equiv p) (zeta p) = ⋯.toInteger
Theorem: CyclotomicIntegers.equiv_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
⊢ (equiv p) (zeta p) = ⋯.toInteger
Tactic:
letI : Fact (Nat.Prime p') := hpri
Proof state after:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ (equiv p) (zeta p) = ⋯.toInteger
Theorem: CyclotomicIntegers.equiv_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ (equiv p) (zeta p) = ⋯.toInteger
Tactic:
rw [equiv_apply, zeta]
Proof state after:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ (AdjoinRoot.liftHom (cyclotomic p ℤ) ⋯.toInteger ⋯) (AdjoinRoot.root (cyclotomic p ℤ)) = ⋯.toInteger
Theorem: CyclotomicIntegers.equiv_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ (AdjoinRoot.liftHom (cyclotomic p ℤ) ⋯.toInteger ⋯) (AdjoinRoot.root (cyclotomic p ℤ)) = ⋯.toInteger
Tactic:
simp only [AdjoinRoot.liftHom_root, IsPrimitiveRoot.integralPowerBasis'_gen]
Proof state after:
no goals
Theorem: CyclotomicIntegers.prime_one_sub_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ Prime (1 - zeta p)
Tactic:
rw [← prime_units_mul (a := -1), Units.val_neg, Units.val_one, neg_mul, one_mul, neg_sub]
Proof state after:
p : ℕ
hpri : Fact p.Prime
⊢ Prime (zeta p - 1)
Theorem: CyclotomicIntegers.prime_one_sub_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ Prime (zeta p - 1)
Tactic:
apply (equiv p).toMulEquiv.prime_iff.mpr
Proof state after:
p : ℕ
hpri : Fact p.Prime
⊢ Prime ((equiv p).toMulEquiv (zeta p - 1))
Theorem: CyclotomicIntegers.prime_one_sub_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ Prime ((equiv p).toMulEquiv (zeta p - 1))
Tactic:
simp only [RingEquiv.toMulEquiv_eq_coe, RingEquiv.coe_toMulEquiv,
  (equiv p).map_sub, (equiv p).map_one, equiv_zeta]
Proof state after:
p : ℕ
hpri : Fact p.Prime
⊢ Prime (⋯.toInteger - 1)
Theorem: CyclotomicIntegers.prime_one_sub_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ Prime (⋯.toInteger - 1)
Tactic:
letI p' : ℕ+ := ⟨p, hpri.out.pos⟩
Proof state after:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
⊢ Prime (⋯.toInteger - 1)
Theorem: CyclotomicIntegers.prime_one_sub_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
⊢ Prime (⋯.toInteger - 1)
Tactic:
letI : Fact (Nat.Prime p') := hpri
Proof state after:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ Prime (⋯.toInteger - 1)
Theorem: CyclotomicIntegers.prime_one_sub_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ Prime (⋯.toInteger - 1)
Tactic:
letI H := IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
Proof state after:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
H : IsPrimitiveRoot (IsCyclotomicExtension.zeta p' ℚ (CyclotomicField p' ℚ)) ↑p' :=
  IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
⊢ Prime (⋯.toInteger - 1)
Theorem: CyclotomicIntegers.prime_one_sub_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
H : IsPrimitiveRoot (IsCyclotomicExtension.zeta p' ℚ (CyclotomicField p' ℚ)) ↑p' :=
  IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
⊢ Prime (⋯.toInteger - 1)
Tactic:
exact H.zeta_sub_one_prime'
Proof state after:
no goals
Theorem: CyclotomicIntegers.one_sub_zeta_mem_nonZeroDivisors
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ∈ nonZeroDivisors (CyclotomicIntegers p)
Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero]
Proof state after:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ≠ 0
Theorem: CyclotomicIntegers.one_sub_zeta_mem_nonZeroDivisors
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ≠ 0
Tactic:
exact (prime_one_sub_zeta p).1
Proof state after:
no goals
Theorem: CyclotomicIntegers.one_sub_zeta_dvd_int_iff
Proof state before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n
Tactic:
letI p' : ℕ+ := ⟨p, hpri.out.pos⟩
Proof state after:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n
Theorem: CyclotomicIntegers.one_sub_zeta_dvd_int_iff
Proof state before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n
Tactic:
letI : Fact (PNat.Prime p') := hpri
Proof state after:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n
Theorem: CyclotomicIntegers.one_sub_zeta_dvd_int_iff
Proof state before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n
Tactic:
letI H := IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
Proof state after:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
H : IsPrimitiveRoot (IsCyclotomicExtension.zeta p' ℚ (CyclotomicField p' ℚ)) ↑p' :=
  IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n
Theorem: CyclotomicIntegers.one_sub_zeta_dvd_int_iff
Proof state before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
H : IsPrimitiveRoot (IsCyclotomicExtension.zeta p' ℚ (CyclotomicField p' ℚ)) ↑p' :=
  IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
⊢ 1 - zeta p ∣ ↑n ↔ ↑p ∣ n
Tactic:
rw [← map_dvd_iff (equiv p), map_sub, map_one, equiv_zeta, map_intCast,
  ← neg_dvd, neg_sub]
Proof state after:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
H : IsPrimitiveRoot (IsCyclotomicExtension.zeta p' ℚ (CyclotomicField p' ℚ)) ↑p' :=
  IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
⊢ ⋯.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n
Theorem: CyclotomicIntegers.one_sub_zeta_dvd_int_iff
Proof state before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact p'.Prime := hpri
H : IsPrimitiveRoot (IsCyclotomicExtension.zeta p' ℚ (CyclotomicField p' ℚ)) ↑p' :=
  IsCyclotomicExtension.zeta_spec p' ℚ (CyclotomicField p' ℚ)
⊢ ⋯.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n
Tactic:
exact zeta_sub_one_dvd_Int_iff H
Proof state after:
no goals
Theorem: CyclotomicIntegers.one_sub_zeta_dvd
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ∣ ↑p
Tactic:
show 1 - zeta p ∣ (p : ℤ)
Proof state after:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ∣ ↑↑p
Theorem: CyclotomicIntegers.one_sub_zeta_dvd
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ 1 - zeta p ∣ ↑↑p
Tactic:
rw [one_sub_zeta_dvd_int_iff]
Proof state after:
no goals
Theorem: CyclotomicIntegers.isCoprime_one_sub_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
hn : ¬↑p ∣ n
⊢ IsCoprime (1 - zeta p) ↑n
Tactic:
apply (((Nat.prime_iff_prime_int.mp hpri.out).coprime_iff_not_dvd.mpr hn).map
  (algebraMap ℤ <| CyclotomicIntegers p)).of_isCoprime_of_dvd_left
Proof state after:
p : ℕ
hpri : Fact p.Prime
n : ℤ
hn : ¬↑p ∣ n
⊢ 1 - zeta p ∣ (algebraMap ℤ (CyclotomicIntegers p)) ↑p
Theorem: CyclotomicIntegers.isCoprime_one_sub_zeta
Proof state before:
p : ℕ
hpri : Fact p.Prime
n : ℤ
hn : ¬↑p ∣ n
⊢ 1 - zeta p ∣ (algebraMap ℤ (CyclotomicIntegers p)) ↑p
Tactic:
exact one_sub_zeta_dvd p
Proof state after:
no goals
Theorem: CyclotomicIntegers.exists_dvd_int
Proof state before:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ∃ m, m ≠ 0 ∧ n ∣ ↑m
Tactic:
refine ⟨Algebra.norm ℤ ((equiv p) n), by simpa, ?_⟩
Proof state after:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ n ∣ ↑((Algebra.norm ℤ) ((equiv p) n))
Theorem: CyclotomicIntegers.exists_dvd_int
Proof state before:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ n ∣ ↑((Algebra.norm ℤ) ((equiv p) n))
Tactic:
rw [← map_dvd_iff (equiv p), map_intCast]
Proof state after:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ (equiv p) n ∣ ↑((Algebra.norm ℤ) ((equiv p) n))
Theorem: CyclotomicIntegers.exists_dvd_int
Proof state before:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ (equiv p) n ∣ ↑((Algebra.norm ℤ) ((equiv p) n))
Tactic:
convert RingOfIntegers.dvd_norm ℚ (equiv p n) using 1
Proof state after:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ↑((Algebra.norm ℤ) ((equiv p) n)) =
    (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ((RingOfIntegers.norm ℚ) ((equiv p) n))
Theorem: CyclotomicIntegers.exists_dvd_int
Proof state before:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ↑((Algebra.norm ℤ) ((equiv p) n)) =
    (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ((RingOfIntegers.norm ℚ) ((equiv p) n))
Tactic:
ext1
Proof state after:
case h.e'_4.h
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ↑↑((Algebra.norm ℤ) ((equiv p) n)) =
    ↑((algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ((RingOfIntegers.norm ℚ) ((equiv p) n)))
Theorem: CyclotomicIntegers.exists_dvd_int
Proof state before:
case h.e'_4.h
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ↑↑((Algebra.norm ℤ) ((equiv p) n)) =
    ↑((algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ((RingOfIntegers.norm ℚ) ((equiv p) n)))
Tactic:
exact DFunLike.congr_arg (algebraMap ℚ _) (Algebra.coe_norm_int (equiv p n))
Proof state after:
no goals
Theorem: CyclotomicIntegers.exists_dvd_int
Proof state before:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ (Algebra.norm ℤ) ((equiv p) n) ≠ 0
Tactic:
simpa
Proof state after:
no goals
Theorem: CyclotomicIntegers.powerBasis_dim
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ (powerBasis p).dim = p - 1
Tactic:
simp [powerBasis, Nat.totient_prime hpri.out, natDegree_cyclotomic]
Proof state after:
no goals
Theorem: CyclotomicIntegers.nontrivial
Proof state before:
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
⊢ Nontrivial (CyclotomicIntegers p)
Tactic:
apply Ideal.Quotient.nontrivial
Proof state after:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
⊢ Ideal.span {cyclotomic p ℤ} ≠ ⊤
Theorem: CyclotomicIntegers.nontrivial
Proof 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]
Proof state after:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
⊢ ¬IsUnit (cyclotomic p ℤ)
Theorem: CyclotomicIntegers.nontrivial
Proof state before:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
⊢ ¬IsUnit (cyclotomic p ℤ)
Tactic:
intro h
Proof state after:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
h : IsUnit (cyclotomic p ℤ)
⊢ False
Theorem: CyclotomicIntegers.nontrivial
Proof 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
Proof state after:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
h : IsUnit (cyclotomic p ℤ)
this : (cyclotomic p ℤ).natDegree = 0
⊢ False
Theorem: CyclotomicIntegers.nontrivial
Proof 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
Proof state after:
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
h : IsUnit (cyclotomic p ℤ)
this : p.totient = 0
⊢ False
Theorem: CyclotomicIntegers.nontrivial
Proof 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)
Proof state after:
no goals
Theorem: CyclotomicIntegers.sum_zeta_pow
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ ∑ i ∈ Finset.range p, zeta p ^ i = 0
Tactic:
rw [← AdjoinRoot.aeval_root (Polynomial.cyclotomic p ℤ), ← zeta]
Proof state after:
p : ℕ
hpri : Fact p.Prime
⊢ ∑ i ∈ Finset.range p, zeta p ^ i = (aeval (zeta p)) (cyclotomic p ℤ)
Theorem: CyclotomicIntegers.sum_zeta_pow
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ ∑ i ∈ Finset.range p, zeta p ^ i = (aeval (zeta p)) (cyclotomic p ℤ)
Tactic:
simp [Polynomial.cyclotomic_prime ℤ p]
Proof state after:
no goals
Theorem: CyclotomicIntegers.zeta_pow_sub_one
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) = -∑ i : Fin (p - 1), zeta p ^ ↑i
Tactic:
rw [eq_neg_iff_add_eq_zero]
Proof state after:
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) + ∑ i : Fin (p - 1), zeta p ^ ↑i = 0
Theorem: CyclotomicIntegers.zeta_pow_sub_one
Proof state before:
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) + ∑ i : Fin (p - 1), zeta p ^ ↑i = 0
Tactic:
convert CyclotomicIntegers.sum_zeta_pow p
Proof state after:
case h.e'_2
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) + ∑ i : Fin (p - 1), zeta p ^ ↑i = ∑ i ∈ Finset.range p, zeta p ^ i
Theorem: CyclotomicIntegers.zeta_pow_sub_one
Proof state before:
case h.e'_2
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) + ∑ i : Fin (p - 1), zeta p ^ ↑i = ∑ i ∈ Finset.range p, zeta p ^ i
Tactic:
conv_rhs => enter [1]; rw [← tsub_add_cancel_of_le hpri.out.one_lt.le]
Proof state after:
case h.e'_2
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) + ∑ i : Fin (p - 1), zeta p ^ ↑i = ∑ i ∈ Finset.range (p - 1 + 1), zeta p ^ i
Theorem: CyclotomicIntegers.zeta_pow_sub_one
Proof state before:
case h.e'_2
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) + ∑ i : Fin (p - 1), zeta p ^ ↑i = ∑ i ∈ Finset.range (p - 1 + 1), zeta p ^ i
Tactic:
rw [Finset.sum_range_succ, add_comm, Fin.sum_univ_eq_sum_range]
Proof state after:
no goals
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof state before:
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
inst✝²⁶ : CommRing A
inst✝²⁵ : Field K
inst✝²⁴ : CommRing B
inst✝²³ : Field L
inst✝²² : Algebra A K
inst✝²¹ : Algebra B L
inst✝²⁰ : Algebra A B
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : IsScalarTower A B L
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
obtain ⟨a, ha⟩ := (pow_dvd_pow _ (Nat.sub_le e 1)).trans hP
Proof state after:
case intro
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
inst✝²⁶ : CommRing A
inst✝²⁵ : Field K
inst✝²⁴ : CommRing B
inst✝²³ : Field L
inst✝²² : Algebra A K
inst✝²¹ : Algebra B L
inst✝²⁰ : Algebra A B
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : IsScalarTower A B L
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
⊢ P ^ (e - 1) ∣ differentIdeal A B
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof state before:
case intro
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
inst✝²⁶ : CommRing A
inst✝²⁵ : Field K
inst✝²⁴ : CommRing B
inst✝²³ : Field L
inst✝²² : Algebra A K
inst✝²¹ : Algebra B L
inst✝²⁰ : Algebra A B
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : IsScalarTower A B L
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
have hp' := (Ideal.map_eq_bot_iff_of_injective
  (NoZeroSMulDivisors.algebraMap_injective A B)).not.mpr hp
Proof state after:
case intro
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
inst✝²⁶ : CommRing A
inst✝²⁵ : Field K
inst✝²⁴ : CommRing B
inst✝²³ : Field L
inst✝²² : Algebra A K
inst✝²¹ : Algebra B L
inst✝²⁰ : Algebra A B
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : IsScalarTower A B L
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof state before:
case intro
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
inst✝²⁶ : CommRing A
inst✝²⁵ : Field K
inst✝²⁴ : CommRing B
inst✝²³ : Field L
inst✝²² : Algebra A K
inst✝²¹ : Algebra B L
inst✝²⁰ : Algebra A B
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : IsScalarTower A B L
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
have habot : a ≠ ⊥ := fun ha' ↦ hp' (by simpa [ha'] using ha)
Proof state after:
case intro
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
inst✝²⁶ : CommRing A
inst✝²⁵ : Field K
inst✝²⁴ : CommRing B
inst✝²³ : Field L
inst✝²² : Algebra A K
inst✝²¹ : Algebra B L
inst✝²⁰ : Algebra A B
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : IsScalarTower A B L
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof state before:
case intro
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
inst✝²⁶ : CommRing A
inst✝²⁵ : Field K
inst✝²⁴ : CommRing B
inst✝²³ : Field L
inst✝²² : Algebra A K
inst✝²¹ : Algebra B L
inst✝²⁰ : Algebra A B
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : IsScalarTower A B L
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
have hPbot : P ≠ ⊥ := by
  rintro rfl; apply hp'
  rwa [← Ideal.zero_eq_bot, zero_pow he, zero_dvd_iff, Ideal.zero_eq_bot] at hP
Proof state after:
case intro
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
inst✝²⁶ : CommRing A
inst✝²⁵ : Field K
inst✝²⁴ : CommRing B
inst✝²³ : Field L
inst✝²² : Algebra A K
inst✝²¹ : Algebra B L
inst✝²⁰ : Algebra A B
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : IsScalarTower A B L
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B