not_exists_int_prime_dvd_sub_of_prime_pow_ne_two

English

In a cyclotomic extension with order p^(k+1) not equal to 2, there is no integer n such that p divides hζ.toInteger − n in the ring of integers.

Русский

В циклотомическом расширении с порядком p^(k+1) ≠ 2 нет целого числа n, чтобы p делило hζ.toInteger − n в кольце целых.

LaTeX

$$¬∃ n : ℤ, (p : 𝓞K) ∣ (hζ.toInteger − n : 𝓞K)$$

Lean4

/-- In a `p ^ (k + 1)`-th cyclotomic extension of `ℚ `, we have that `ζ` is not congruent to an
  integer modulo `p` if `p ^ (k  + 1) ≠ 2`. -/
theorem not_exists_int_prime_dvd_sub_of_prime_pow_ne_two [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (htwo : p ^ (k + 1) ≠ 2) :
    ¬(∃ n : ℤ, (p : 𝓞 K) ∣ (hζ.toInteger - n : 𝓞 K)) :=
  by
  intro
    ⟨n, x, h⟩
      -- Let `pB` be the power basis of `𝓞 K` given by powers of `ζ`.

  let pB := hζ.integralPowerBasis
  have hdim : pB.dim = p ^ k * (↑p - 1) := by
    simp [integralPowerBasis_dim, pB, Nat.totient_prime_pow hp.1 (Nat.zero_lt_succ k)]
  replace hdim : 1 < pB.dim := by
    rw [Nat.one_lt_iff_ne_zero_and_ne_one, hdim]
    refine
      ⟨by
        simp only [ne_eq, mul_eq_zero, NeZero.ne _, Nat.sub_eq_zero_iff_le, false_or, not_le, Nat.Prime.one_lt hp.out],
        ne_of_gt ?_⟩
    by_cases hk : k = 0
    · simp only [hk, zero_add, pow_one, pow_zero, one_mul, Nat.lt_sub_iff_add_lt, Nat.reduceAdd] at htwo ⊢
      exact htwo.symm.lt_of_le hp.1.two_le
    ·
      exact
        one_lt_mul_of_lt_of_le (one_lt_pow₀ hp.1.one_lt hk)
          (have := Nat.Prime.two_le hp.out;
          by cutsat)
  rw [sub_eq_iff_eq_add] at h
  replace h := pB.basis.ext_elem_iff.1 h ⟨1, hdim⟩
  have := pB.basis_eq_pow ⟨1, hdim⟩
  rw [hζ.integralPowerBasis_gen] at this
  simp only [PowerBasis.coe_basis, pow_one] at this
  rw [← this, show pB.gen = pB.gen ^ (⟨1, hdim⟩ : Fin pB.dim).1 by simp, ← pB.basis_eq_pow,
    pB.basis.repr_self_apply] at h
  simp only [↓reduceIte, map_add, Finsupp.coe_add, Pi.add_apply] at h
  rw [show (p : 𝓞 K) * x = (p : ℤ) • x by simp, ← pB.basis.coord_apply, LinearMap.map_smul, ← zsmul_one, ←
    pB.basis.coord_apply, LinearMap.map_smul, show 1 = pB.gen ^ (⟨0, by cutsat⟩ : Fin pB.dim).1 by simp, ←
    pB.basis_eq_pow, pB.basis.coord_apply, pB.basis.coord_apply, pB.basis.repr_self_apply] at h
  simp only [smul_eq_mul, Fin.mk.injEq, zero_ne_one, ↓reduceIte, mul_zero, add_zero] at h
  exact (Int.prime_iff_natAbs_prime.2 (by simp [hp.1])).not_dvd_one ⟨_, h⟩

Похожие утверждения