Irreducible

Stream: new members

[vxctyxeha]

I proved that if n
is a prime, then p(x)=xn−1+⋯+x+1
is irreducible over Z
But how to split a and b? Is there such an equation in mathlib?

import Mathlib

open Polynomial Nat

theorem irreducible_geom_sum_iff_prime (p : ℕ) (hp_ge_2 : 2 ≤ p) :
    Fact p.Prime ↔ Irreducible (∑ i ∈ Finset.range p, X ^ i : ℤ[X]) := by
  constructor
  · -- 方向 1: Fact p.Prime → Irreducible (∑ X^i)
    intro hp_fact -- hp_fact : Fact p.Prime
    rw [← (@cyclotomic_prime ℤ _ p hp_fact)]
    apply cyclotomic.irreducible
    exact Nat.Prime.pos hp_fact.out

  intro h_irred_sum -- h_irred_sum : Irreducible (∑ i ∈ Finset.range p, X ^ i)
  have p_is_prime : p.Prime :=by
    by_contra h_not_prime_p_proof
    obtain ⟨a, ha_dvd_p, ha_one_lt_a, ha_lt_p⟩ : ∃ a, a ∣ p ∧ 1 < a ∧ a < p :=
        Nat.exists_dvd_of_not_prime2 hp_ge_2 h_not_prime_p_proof
    obtain ⟨b, p_eq_ab⟩ := exists_eq_mul_left_of_dvd ha_dvd_p
    have hb_one_lt_b : 1 < b :=by
      rw [p_eq_ab] at ha_lt_p
      by_cases h_b_is_zero : b = 0
      rw [h_b_is_zero] at p_eq_ab; linarith [p_eq_ab, hp_ge_2];exact one_lt_of_lt_mul_left ha_lt_p
    rw [p_eq_ab] at h_irred_sum
    rw [← geom_sum₂_with_one ] at h_irred_sum
    simp only [one_pow, mul_one] at h_irred_sum

[Aaron Liu]

Can you tell me exactly what you mean by "split"? What do you want to split?

[vxctyxeha]

image.png
i need to prove contradiction

[Aaron Liu]

import Mathlib

-- What should I call this? `geom_sum_mul` is taken.
example {R : Type*} [Semiring R] (x : R) (n m : ℕ) :
    ∑ i ∈ Finset.range (n * m), x ^ i = ∑ i ∈ Finset.range m, x ^ i * ∑ i ∈ Finset.range n, (x ^ m) ^ i := by
  rw [← Fin.sum_univ_eq_sum_range, ← finProdFinEquiv.sum_comp, Fintype.sum_prod_type]
  simp_rw [finProdFinEquiv_apply_val, pow_add, pow_mul, ← Finset.sum_mul, ← Finset.mul_sum, Fin.sum_univ_eq_sum_range]

[vxctyxeha]

is it true ?0 < (∑ i ∈ Finset.range a, X ^ i).degree

[Aaron Liu]

It's not true for a = 0 and a = 1

[Jz Pan]

Aaron Liu said:

What should I call this? geom_sum_mul is taken.

Maybe geom_sum_mul_eq_geom_sum_mul_geom_sum

[vxctyxeha]

thanks